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
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
