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

David MENTRE dmentre at linux-france.org
Thu Aug 18 18:00:13 CEST 2016

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:

Thank you for the help!

Best regards,

More information about the Why3-club mailing list