Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Sort Mismatch in Model

Tags:

z3

I have analyzed a formula in QF_AUFLIA with z3. The result was sat. The model returned by (get-model) contained the following lines:

  (define-fun PCsc5_ () Int
    (ite (= 2 false) 23 33)

According to my understanding of the SMTLIBv2 language, this statement is malformed. = should only be applied to arguments of the same sort. However, 2 has sort Int and false has sort Bool.

When I feed back just these two lines to z3, it agrees with me by saying:

invalid function application, sort mismatch on argument at position 2

Is this a bug?

If not, how am I supposed to interpret (= 2 false)?

like image 909
Georg Avatar asked Jan 03 '12 10:01

Georg


1 Answers

The problem was due to a type error in the input. Z3 3.2 misses some type errors in macro applications. This problem was fixed. The next release will correctly report the type error (aka sort mismatch). Here is a minimal example that exposes the problem:

(set-option :produce-models true)
(declare-fun q (Int) Bool)
;; p1 is a macro
(define-fun p1 ((z Int) (y Int)) Bool
  (ite (q y) (= z 0) (= z 1)))
(declare-const a Int)
(declare-const b Bool)
(assert (p1 a b)) ;; << TYPE ERROR: b must be an Int
(check-sat)
(get-model) 
like image 164
Leonardo de Moura Avatar answered Oct 12 '22 03:10

Leonardo de Moura