时间戳

首页 > 解决方案 > 当断言 0 除以 0 为 1 时，z3 返回未知

z3 - 当断言 0 除以 0 为 1 时，z3 返回未知

问题描述

我正在尝试文章Z3: a tutorial中的示例。有一个例子展示了所有的函数都是总的，包括“div”：

(push)
(assert (= 1 (div 0 0))) 
(check-sat)
;sat (pop)

我注意到 z3 版本 4.8.5 根据是否使用“推送”返回不同的结果。

使用下面的代码，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”的使用应该不会导致不同的结果，因为只有一个断言？

标签： z3

解决方案

严格来说unknown并不sat矛盾：求解器可以随时退出并说unknown. 例如，如果您明确使用策略，则可能会发生这种行为。

但是你是绝对正确的，这push是导致这种差异的奇怪现象。请在 z3 github 问题站点提交工单：https ://github.com/Z3Prover/z3/issues ，让我们知道您发现了什么！

推荐阅读