Почему результат запроса изменяется, если комментарий является промежуточным вызовом `(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 как:

(декларируют-типы данных() ((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_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7)))

Заявление выше, по существу, определяющее два "перечисление" типов. С этими объявлениями вы получите согласованный ответ для второго запроса.