Hi Arnaud,
for any possible integer value, there exists a value of your myRecord
type holding that value. So, your value_axiom axiom states,
essentially, that all integers are greater than one, which is false.
Having a false axiom makes every proof obligation trivially provable,
just as your example shows.
Best,
Andrei
On 13 October 2014 20:26, arnaud <arnaud.dieumeg...@enseeiht.fr> wrote:
> 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
> Why3-club@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
