CODEWITHSUNDEEP
z3why3
Virgile
Virgile

Reputation: 10148

z3 4.3.2 fails to find a model for Why3-generated (satisfiable) goals

I'm trying to use Why3's Z3 back-end in order to retrieve models that can then be used to derive test cases exhibiting bugs in programs. However, Z3 version 4.3.2 seems unable to answer sat for any Why3 goal. It looks like some of the axiomatic definitions used by Why3 somehow confuse Z3. For instance, the following example (which is a tiny part of what Why3 generates)

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

(check-sat)

results in timeout with the following command line:

z3 -smt2 model.partial=true file.smt2 -T:10

On the other hand, changing the definition to

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x))))

  (assert
  (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))

will get me a model (which looks pretty reasonable)

(model 
  (define-fun abs1 ((x!1 Int)) Int
    (ite (>= x!1 0) x!1 (* (- 1) x!1)))
)

but if I try to add the next axiom present in the original Why3 file, namely

;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))

again Z3 answers timeout.

Is there something I'm missing in the configuration of Z3? Moreover, in previous versions of Why3, there was an option MODEL_ON_TIMEOUT, which allowed to retrieve a model in such circumstances. Even though there was no guarantee that this was a real model since Z3 could not finish to check it, in practice such models generally contained all the information I needed. However, I haven't found a similar option in 4.3.2. Does it still exist?

Update The last axiom Abs_pos was wrong (I toyed a bit with Why3's output before posting here and ended up pasting an incorrect version of the issue). This is now fixed.

Upvotes: 1

Views: 133

Answers (1)

J&#246;rg Pf&#228;hler
J&#246;rg Pf&#228;hler

Reputation: 29

The additional axiom

(assert (not (forall ((x Int)) (<= 0 (abs1 x)))))

makes the problem unsatisfiable, since abs1 always returns a non-negative integer and with the additional axiom you require the existence of a negative result for abs1 for some x. The web version of Z3 returns unsat as expected, see here.

Upvotes: 0

Related Questions