[Why3-club] Problem with yices

Andrei Paskevich andrei at lri.fr
Fri Feb 10 11:11:15 CET 2012


On Fri, Feb 10, 2012 at 07:53, Benjamin Gregoire
<Benjamin.Gregoire at inria.fr> wrote:
> Hi,
>   Santiago Zanella sends me the following example:
>
> theory FOO
>  use import int.Int
>  lemma foo : 0<  -1
> end
>
> # why3 -P yices foo.why -T FOO -G foo
> foo.why FOO foo : Valid (0.01s)
>
> It looks like a strange behavior of Yices.
> Do you have a idea of what happens ?
>  Benjamin Grégoire

Fixed in 5e8e081 in Why3 git.

Best,
Andrei



More information about the Why3-club mailing list