--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on August 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C/WP and CVC4 (version 1.5)



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                    |