"the check fails with all inputs" in a counter-example value
Hello all,
it seems that we found a bug in the management of counterexamples.
When generating and proving a mlw file analog to the following one via the API, we got the message:
This seems to be a bug:
process model value : the check fails with all inputs = Unparsed()
(please report)
This seems related to the fact of having an assert before a loop with an invariant (whose formula is, in our case, the same as the one of the assert).
Here is the minimal example:
module Bug
use export ref.Ref
use export bool.Bool
val m1 [@model] [@model_trace:M1] : ref bool
let bug ()
diverges
=
m1 := False;
assert { not (!m1) };
while (true)
do
invariant { not (!m1) }
m1 := True;
done
end
We used CVC4,1.5,counterexamples and had the following output when using Why3 via command-line:
____ why3 prove -P CVC4,1.5,counterexamples bug_ce_parsing_min.mlw
File bug_ce_parsing_min.mlw:
Verification condition bug'vc.
Prover result is: Unknown (unknown) (0.01s, 1103 steps).
The following counterexample model has not been verified
(not checking CE model, missing option --check-ce):
File bug_ce_parsing_min.mlw:
Line 11:
M1 = false
Line 12:
the check fails with all inputs
Line 13:
M1 = false
Line 15:
M1 = true
Line 16:
M1 = true
Thanks in advance