--- layout: fc_discuss_archives title: Message 8 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)



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