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
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 examp
-- Andrei Paskevich (2014-10-13)
>
> 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.
Hi Arnaud,
That's a usual problem when y
Hi Andrei, Yannick,
It seems that my problem was more human related than software related !
Thanks for these very helpful informations.
Indeed you are right I'm trying to translate some data structure and I
have to deal with such problems.
I will have a look at these and thanks for the pointers.
