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

David MENTRE dmentre at linux-france.org
Thu Aug 18 18:09:17 CEST 2016


Hello David,

Le 18/08/2016 à 17:51, David Hauzar a écrit :
> Indeed, counterexamples are currently not working with CVC4 1.4 out of
> the box. The driver used for cvc4 1.4 (drivers/cvc4_14) does not include
> the transformation prepare_for_counterexmp which is necessary for
> counterexample generation and sets logic to AUFBVDTNIRA. The driver used
> for cvc 1.5 (drivers/cvc4_15) contains the transformation
> prepare_for_counterexmp (note that this transformation is noop if
> counterexample generation is not selected) and sets logic to
> AUFBVDTLIRA.

Yes, I came to the same conclusion when looking at the differences
between the CVC4 1.4 and 1.5 drivers. Glad to see that I'm getting some
understanding of this machinery. :-)

> This has a bad effect of CVC4 emitting error when a
> non-linear operator is used. 

I'll try to keep that in mind if I get such error.

> That's why in SPARK we use two drivers for
> CVC4 1.5 - one setting the logic to AUFBVDTLIRA for generation of
> counterexamples and one setting the logic to AUFBVDTNIRA for proof.

If I ever go into "production", I'll follow this pattern.

> It would be more convenient for Why3 users if Why3 would force the
> linear arithmetic automatically if counterexample generation is selected.

Another easy path would be do add an additional driver specific to
counter example generation (like done for noBV). I don't mind clicking
on another button to get a counter-example. But multiplying drivers for
the same prover might not be viable when one has several options
(BV/noBV, CE/noCE, ...).

Best regards,
david



More information about the Why3-club mailing list