Hi there,
I'm experiencing some troubles with Why3 and Z3.
I found a small reproducer for my issue:
theory Test
use import int.Int
type myRecord = { value : int }
axiom value_axiom : forall i1 : myRecord. i1.value >= 1
goal test: forall i: myRecord.
1 < i.value
end
If you try to prove this with z3 then it says: Valid.
Which is quite annoying.
I'm using z3 v4.3.1 and Why3 v0.83.
I know that my versions are a little old but for some reasons I cannot
change them easily.
Does anyone knows if this problem is due to:
1 - The Why3 driver ? (maybe it is fixed in a newer version)
2 - Z3 ? (idem)
3 - Me ? (no new version planned)
Thanks for your help
Arnaud
_______________________________________________
Why3-club mailing list
[email protected]
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
