在调试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。
这是量词推理引擎之一的错误。 这个错误会被修正。 在此期间，你能避免使用的数据类型，而不是未解释的种种+基数约束的错误。 也就是说，你声明Q和T为：
（声明-数据类型（）（（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）））
上述声明，基本上限定了两个“枚举”类型的。 有了这些声明，你将获得第二个查询一致的答案。
