z3 - 奇怪的语法错误

Question

只是尝试使用 smtlib。我没有看到以下内容有什么问题...

(set-logic BV)
(declare-fun var1 () (_ BitVec 32)) ; a is a constant
(declare-fun var2 () (_ BitVec 32)) ; a is a constant
(declare-fun var3 () (_ BitVec 32)) ; a is a constant

(assert(
    (= var1 var2)
    and
    (= var3 bvsub(var1 var2) )
    ))
(check-sat)
(get-model)

使用 z3 运行它，错误是：（错误“第 7 行第 2 列：无效的合格/索引标识符，'_' 或 'as' 预期的”）

Answer 1

2次编辑后，终于弄明白了：

(set-logic BV)
(declare-fun var1 () (_ BitVec 32)) ; a is a constant
(declare-fun var2 () (_ BitVec 32)) ; a is a constant
(declare-fun var3 () (_ BitVec 32)) ; a is a constant

(assert(
    and (= var1 var2) (= var3 (bvsub var1 var2))))
(check-sat)
(get-model)