z3 - 如果注释中间 `(check-sat)` 调用，为什么查询结果会更改？

Question

在调试 UNSAT 查询时，我注意到查询状态有一个有趣的差异。查询结构为:

assert(...)
(push)      ; commenting any of these two calls
(check-sat) ; makes the whole query UNSAT, otherwise it is SAT

assert(...)
(check-sat) ; SAT or UNSAT depending on existence of previous call
(exit)

没有 pop在查询中调用。触发此行为的查询是 here .

想法为什么？

注意:我实际上不需要增量，它仅用于调试目的。 Z3 版本是 3.2。

Answer 1

这是量词推理引擎之一中的错误。这个错误将被修复。同时，您可以通过使用数据类型而不是未解释的排序 + 基数约束来避免该错误。也就是说，您声明 Q和 T作为:

(declare-datatypes () ((Q q_accept_S13 q_T0_init q_accept_S7 q_accept_S6 q_accept_S5 q_accept_S4 q_T0_S3 q_accept_S12 q_accept_S10 q_accept_S9 q_accept_all)))

(declare-datatypes () ((T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7)))

上面的声明本质上定义了两种“枚举”类型。
通过这些声明，您将获得第二个查询的一致答案。