Bad counter-example that used to be good
Hello. It looks like a bug has been introduced in the counter-example parser.
use int.Int
use mach.int.Int32
type t = { mutable contents : int32 }
let rec f (x : Int32.int32) : ()
requires { Int.(<) (Int32.to_int x) 1000 } =
let y = { contents = Int32.(+) x 1 } : t in
y.contents <- Int32.(+) y.contents 3;
assert { Int.(<) (Int32.to_int y.contents) 42 };
The assert in this program is wrong. Unfortunately the counter-example returned by Why3 is bad cex. With CVC4
let rec f (x : Int32.int32) : ()
(* x = {int32'int => 39 (0X27)} *)
requires { Int.(<) (Int32.to_int x) 1000 } =
let y = { contents = Int32.(+) x 1 } : t in
(* result of call at line 8, characters 25-38 = {int32'int => 39 (0X27)};
y = {int32'int => 39 (0X27)} *)
y.contents <- Int32.(+) y.contents 3;
(* result of call at line 9, characters 18-40 = {int32'int => 39 (0X27)};
y = {int32'int => 39 (0X27)} *)
assert { Int.(<) (Int32.to_int y.contents) 42 };
(* y = {int32'int => 39 (0X27)} *)
It looks like it has been good a long time and with a git-bisect
I found that !599 (merged) introduced the bug (seems that it comes from 1d4ee370). The prover output being the same before the bug was introduced and after, the problem probably comes from the model parser.