z3 - Z3 公式未通过语法检查

Question

当 x13 在箭头所在的行中被 av5 替换时，以下 SMT 公式在rise4fun 站点的语法检查失败。

(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) 

错误信息是

Z3(8, 26)：错误：无效的函数应用，位置 2 的参数排序不匹配

知道我可能做错了什么吗？

Answer 1

您使用的是哪个版本？我无法使用 4.3.x 版或不稳定（正在进行中）分支重现此问题。在这两种情况下，我都得到unsat. 我也unsat上了rise4fun。