[Why3-club] Problem with yices
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:
> Santiago Zanella sends me the following example:
> theory FOO
> use import int.Int
> lemma foo : 0< -1
> # 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.
More information about the Why3-club