[Why3-club] Count-example generation attempts with Z3 and CVC4

David Hauzar david.hauzar at inria.fr
Thu Aug 18 16:43:36 CEST 2016


Hello David,

On 18.08.2016 16:18, David MENTRE wrote:
> Le 18/08/2016 à 15:59, David MENTRE a écrit :
>> But CVC4 tells me that I have
>> non-linear arithmetic so generation of counter-example is disabled.
>
> In fact, this answer of CVC4 is very strange. On the same
> counter_example_test.mlw file (attached) on which Z3 can generate
> counter examples, CVC4 always answer "non linear arith"!
>
> Any idea on what is going on?
>
> Here is CVC4 (1.4) output I obtain:
> """
> $ why3 prove -C why3.config -L . --get-ce -P cvc4 --debug call_prover
> counter_example_test.mlw

I am able to get counterexamples with CVC4 in your example:

$ why3 prove -L . --get-ce -P CVC4 --debug call_prover example.mlw

Call_provers: exited with status 0
Call_provers: prover output:
unknown
((x1 0))
(:reason-unknown incomplete)

Call_provers: model:
Call_provers: File example.mlw:
Line 10:
x = 0
example.mlw Counter_example WP_parameter f : Unknown (0.01s)
Counter-example model:File example.mlw:
Line 10:
x = 0

...

The section of my why3.config about CVC4 is:

...
[prover]
command = "cvc4 --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "cvc4 --stats --rlimit=%S --lang=smt2 %f"
driver = ".../why3/share/drivers/cvc4_15.drv"
editor = ""
in_place = false
interactive = false
name = "CVC4"
shortcut = "cvc4-15-pre"
version = "1.5-prerelease"
...

I use the following version of CVC4:

$ cvc4 --version

This is CVC4 version 1.5-prerelease
compiled with GCC version 4.9.4 20160529 (for GNAT Pro 17.0w 20160529)
on Jul  1 2016 05:44:27
...

David


More information about the Why3-club mailing list