Rac checker returns incorrect result with expl attr
use int.Int
let f (x : int) : unit =
check { [@expl:e] not (0 <= x \/ x <= 0) };
()
If I run CVC4 in counterexamples mode to prove this program, I get:
$ why3 prove -P CVC4,1.8,counterexamples -L share/ -a split_vc f.mlw
File f.mlw:
Line 2:
x = 0
Line 3:
x = 0
It seems to be a correct counter-example, but the rac says
Prover result is: Unknown (sat) (0.02s, 4743 steps).
Sorry, we don't have a good counterexample for you :(
You can notice that this counter-example can be verified if I remove the attribute [@expl:e]
.