考虑以下 SMTLIB 程序(在rise4fun此处):
(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.arith.nl.gb false)
(declare-const n Int)
(declare-const i Int)
(declare-const r Int)
(assert (= i n))
(assert (= r (* i n)))
(push)
(assert (not (= r (* n n))))
(check-sat) ; unknown
(pop)
尽管它似乎只需要对句法相等进行推理,但 Z3(4.3.2 正式版,以及 4.4.0 b6c40c6c0eaf)仍然未能表明最终断言是unsat
.
出乎意料(至少对我而言),设置smt.arith.nl.gb
为true
使示例验证(即check-sat
产量unsat
)。
对于它的价值,这里有一些进一步的观察:
如果乘法分别更改为或,则可以显示最终断言
unsat
(* i n)
(* n i)
如果将乘法更改为,则无法显示
unsat
(* i i)
(push)
并且(pop)
似乎不会影响示例,即可以将它们删除而不影响所描述的观察结果
这是一个错误还是smt.arith.nl.gb
需要显示此示例的原因unsat
?