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

Это ошибка в одном из механизмов квантификации. Эта ошибка будет исправлена. Тем временем вы можете избежать ошибки, используя типы данных вместо неинтерпретируемых ограничений сортировки + количества элементов. То есть вы заявляете 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)))

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