奇怪的语法错误

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' expected")

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)