The following SMT formula fails syntactic check at rise4fun site 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?
