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

David Hauzar david.hauzar at inria.fr
Thu Aug 18 17:51:37 CEST 2016


Hello David,

On 18.08.2016 17:17, David MENTRE wrote:
> Clearly, the generated SMT2 file does not set logic to AUFLIRA, as shown
> in the used .smt2 file for one goal of my example:
> """
> (set-logic AUFBVDTNIRA)
> ;;; generated by SMT-LIB2 driver
> ;;; SMT-LIB2 driver: bit-vectors, common part
> (set-option :produce-models true)
> ;;; SMT-LIB2: integer arithmetic
> (declare-datatypes () ((tuple0 (Tuple0))))
> ;; CompatOrderMult
>   (assert
>   (forall ((x Int) (y Int) (z Int))
>   (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z))))))
>
> (declare-datatypes () ((s_t (mk_s_t (x Int)(y Int)))))
> (assert
> ;; WP_parameter_f
>  ;; File "counter_example_test.mlw", line 10, characters 6-7
>   (not (forall ((x1 Int)) (< 0 (+ x1 x1)))))
> (check-sat)
> (get-info :reason-unknown)
> /tmp/why_5d496b_counter_example_test-T-WP_parameter_f.smt2 (END)
> """
>
> I'll do some test with CVC4 1.5 that you are using, as suggested by David.

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. This has a bad effect of CVC4 emitting error when a 
non-linear operator is used. 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.

It would be more convenient for Why3 users if Why3 would force the 
linear arithmetic automatically if counterexample generation is 
selected. It would be easy to do this, but on the other side it would be 
a bit temporary hack because we believe that CVC4 should not turn off 
counterexample generation just because the logic is set to non-linear 
arithmetic. And as there was need for this in SPARK it was never 
implemented.

Sorry, this should be documented in the manual (I have already quickly 
written an initial version of such a documentation, but it should be 
probably polished more to be a part of master branch and then official 
release).

David


More information about the Why3-club mailing list