z3 - 理解逻辑上下文

Question

当我在检查后显示我的逻辑上下文时，除其他外，我得到：

inconsistent():1
m_asserted_formulas.inconsistent():1
#1 := true
#2 := false
... (follows around 40 of theses assertions)
#144 := (not #143)
asserted formulas:
#23 #125 .... #2

我了解在断言公式列表中存在一些不一致之处。我看到的第一个是断言 2：

#2 := false

我是对的，还是“错误”是一个真实的断言？

提前致谢，

AG。

Answer 1

是的，false在您的上下文中被断言为真实。请注意，上下文被标记为不一致：inconsistent():1。这里的1意思true和 C 中的一样。请注意，逻辑上下文的这种低级表示只能用于调试目的。它并不是真正用于“外部”消费。最后，false可能没有被用户明确断言，而是由用户执行的断言暗示。