[Why3-club] Problem with yices

Benjamin Gregoire Benjamin.Gregoire at inria.fr
Fri Feb 10 07:53:47 CET 2012


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






More information about the Why3-club mailing list