[Why3-club] Count-example generation attempts with Z3 and CVC4

Yannick Moy moy at adacore.com
Thu Aug 18 16:46:00 CEST 2016

-- David MENTRE (2016-08-18)
> In fact, this answer of CVC4 is very strange. On the same
> counter_example_test.mlw file (attached) on which Z3 can generate
> counter examples, CVC4 always answer "non linear arith"!
> Any idea on what is going on?

CVC4 does not issue counterexamples when non linear arithmetic is used. Hence, for generation of counterexamples, Why3 generates files for CVC4 that force the use of AUFLIRA (the linear arithmetic case) instead of AUFNIRA. If a non-linear operator is used, then CVC4 issues an error, which is probably what happens in your case. But this is not coming from your file, so from int.Int? Can you look at the SMT2 file generated to see where it uses non-linear arithmetic? That's strange, as we do use import int.Int like this in SPARK, without any problem.
Yannick Moy, Senior Software Engineer, AdaCore

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20160818/c005a7c3/attachment-0001.html>

More information about the Why3-club mailing list