Hello David, Le 18/08/2016 à 16:43, David Hauzar a écrit : > I am able to get counterexamples with CVC4 in your example: [...] > I use the following version of CVC4: > > $ cvc4 --version > > This is CVC4 version 1.5-prerelease
I confirm that using CVC4 version 1.5-prerelease counter examples are correctly generated on my example. More precisely, I used this version of CVC4: http://cvc4.cs.nyu.edu/builds/src/cvc4-1.5pre-smtcomp2016.tar.gz Thank you for the help! Best regards, david _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
