--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2017 ---
Hello, in âACSL by Exampleâ (https://fraunhoferfokus.github.io/acsl-by-example/), we have been using the prover CVC4 (http://cvc4.cs.stanford.edu/web/) for quite some time. Recently, a new version (1.5) was released. Unfortunately, it appears that this new version can discharge considerably fewer of our proof obligations than the previous release 1.4. Here is a short list that highlights the issue. Example 1.4 1.5 accumulate 8 1 adjacent_difference 23 0 adjacent_difference_inv 20 3 adjacent_find 9 1 binary_search 2 0 binary_search2 3 0 copy 12 1 copy_backward 12 1 count 10 3 equal 1 1 equal_range 3 0 equal_range2 36 4 I wonder, whether other WP users also observe this problem. Maybe there is fancy option that one should supply to CVC4-1.5 (through why3)? If you know of one, then please let me know! Regards Jens