[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:
  http://cvc4.cs.nyu.edu/builds/src/cvc4-1.5pre-smtcomp2016.tar.gz

Thank you for the help!

Best regards,
david



More information about the Why3-club mailing list