Z3 formula fails syntactic check.

Feb 14, 2013 at 8:18 PM
The following SMT formula fails syntactic check when x13 is replaced by av5 in the line with arrow

(set-info :status unknown)
;(set-logic QF_BV)
(declare-fun in3 () (_ BitVec 16))
(assert
(let ((x8 ((_ zero_extend 16) in3)))
(let ((x13 (ite (not (= x8 ( bv00000000 32))) ( bv00045069 32) (_ bv00000174 32))))
(let ((av5 (= x13 (_ bv00045069 32))))
(= x13 (_ bv4294967295 32)))))) <---------
(assert true)
(check-sat)

The error message is

Z3(8, 26): ERROR: invalid function application, sort mismatch on argument at position 2

Any idea what I might I be doing wrong?
Coordinator
Feb 14, 2013 at 8:49 PM