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

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


Hello Yannick,

Le 18/08/2016 à 16:46, Yannick Moy a écrit :
> Hence, for generation of counterexamples, Why3 generates files for CVC4
> that force the use of AUFLIRA (the linear arithmetic case) instead of
> AUFNIRA. If a non-linear operator is used, then CVC4 issues an error,
> which is probably what happens in your case. But this is not coming from
> your file, so from int.Int? Can you look at the SMT2 file generated to
> see where it uses non-linear arithmetic?

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.

Best regards,
david



More information about the Why3-club mailing list