cvc4 modeling error in tutorial about ivory HOT 7 CLOSED

After some more debugging (using asserts in the concrete syntax, and no function call to inline) we still see the issue, but commenting out the inner most if-statement the model checker can find a proof.

from ivory.

It's been a while since I looked at the model checker, but this line

looks suspicious to me.

It should probably be sets_ (\s -> s { symCond = b' &&. b }) to track nested if-statements, which is exactly the scenario here.

from ivory.

Thanks, you're probably right but I just tried it and I'm still getting unsafe. We'll dig deeper tomorrow.

Thanks!

from ivory.

Ah, @leepike and I had talked about the nested if stuff, but we must have never made the change that @gridaphobe mentioned above.

from ivory.

Actually, that's probably a separate bug. Digging in a bit more I noticed a few things

1. These two assertions correspond to the two branches of the inner if-statement, but the 2nd refers to the variable set by the first. That's totally bogus!

ASSERT ((deref2 + 25) < deref4) => (mc_2var0 = (mc_1var0 WITH .mp := deref2 + 25)) ;     % [ No location available ];
ASSERT (NOT ((deref2 + 25) < deref4)) => (mc_3var0 = (mc_2var0 WITH .mp := deref4)) ;    % [ No location available ];

If you rewrite the 2nd line to

ASSERT (NOT ((deref2 + 25) < deref4)) => (mc_3var0 = (mc_1var0 WITH .mp := deref4)) ;    % [ No location available ];

the query is valid.

1. My copy of cvc 1.4 choked on mc_1var0 WITH .mp := deref2 + 25, it seemed to want extra parentheses around deref2 + 25.

from ivory.

So this is a bug in the translation to cvc4. We need to restore the latest references when we return from inBranch.

from ivory.

Closing this, as we're rewriting the model checker (@eddywestbook).

from ivory.