--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on August 2017 ---
Hi to all, I'd like to add a follow-up to this thread about CVC4 1.5. If you are experimenting with CVC4 1.5 via Why3 0.87.3 or earlier, then you should be aware that the driver file cvc4_15.drv distributed with Why3 0.87.3 is NOT suitable for use with the release 1.5 of CVC4. This driver was designed for use with pre-releases of CVC4 1.5, and specifically to exploit model generation so as to produce counterexamples. Thus, if you want to add a support for CVC4 1.5 in your personal why3.conf file, then I strongly recommend to keep using the driver cvc4_14.drv designed for 1.4 In particular, any benchmark comparing 1.4 and 1.5 should be done using the same driver. Notice there is a slightly enhanced driver for CVC4 1.5 in the master branch of Why3 development (git repository), compiling and using the version is a perfectly acceptable alternative, while waiting fir the next Why3 release. - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |