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)
?
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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With