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调用。触发此行为的查询在此处。

想法为什么？

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

Answer 1

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

（声明数据类型（）（（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）））

（声明数据类型（）（（T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7）））

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