我在尝试Z3: a tutorial这篇文章中的例子。有一个例子说明所有的函数都是合计的,包括"div":
(push)
(assert (= 1 (div 0 0)))
(check-sat)
;sat (pop)
我注意到z3版本4.8.5根据用户是否使用"push“返回不同的结果。
使用以下代码,z3将返回未知:
(get-info :version)
;(push)
(assert (= 1 (div 0 0)))
(check-sat)
z3的输出为:
(:version "4.8.5 - build hashcode 8c085f1a1850")
unknown
相比之下,使用以下代码,z3将返回sat:
(get-info :version)
(push)
(assert (= 1 (div 0 0)))
(check-sat)
(get-model)
z3的输出为:
(:version "4.8.5 - build hashcode 8c085f1a1850")
sat
(model
)
在rise4fun教程中,它说“命令push通过保存当前堆栈大小创建一个新的作用域”,似乎"push“的使用在这里不应该导致不同的结果,因为只有一个断言?
发布于 2019-05-29 13:43:07
严格地说,unknown
和sat
并不矛盾:求解器可以随时退出并说unknown
。例如,如果您显式地使用策略,就会发生这种行为。
但是你是绝对正确的,奇怪的push
导致了这种差异。请在z3 github issues站点:https://github.com/Z3Prover/z3/issues提交罚单,并让我们知道您发现了什么!
https://stackoverflow.com/questions/56348003
复制相似问题