-- 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
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
