Why does a query result changes if comment an intermediate `(check-sat)` call?
Question
While debugging UNSAT query I noticed an interesting difference in the query status. The query structure is:
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)
There are no pop
calls in the query. The query that triggers this behaviour is here.
Ideas why?
Note: I don't actually need incrementality, it is for debugging purposes only. Z3 version is 3.2.
Solution
This is a bug in one of the quantifier reasoning engines. This bug will be fixed. In the meantime, you can avoid the bug by using datatypes instead of uninterpreted sorts + cardinality constraints. That is, you declare Q
and T
as:
(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)))
The declarations above are essentially defining two "enumeration" types. With these declarations, you will get a consistent answer for the second query.