Я скачал твой пример.Указанная логика неверна, команда:
(set-logic QF_AUFLIA)
Эта логика указывает, что скрипт будет содержать только массивы, неинтерпретированные функции и целочисленные переменные, инет квантификаторов.Тем не менее, он содержит реальные переменные.Если вы удалите эту команду, вы получите правильный ответ (sat) в обоих случаях.Вы получили другой ответ при использовании PROOF_MODE = 1, потому что некоторые препроцессоры в Z3 не поддерживают генерацию пробных изображений, тогда они отключаются, когда включена пробная генерация.
При этом мы исправили много ошибок в Z3 2.19.Новая версия 3.0 будет выпущена в ближайшее время.Вы уже можете использовать предварительную версию, которую мы представили для SMT-COMP .