Как прокомментировал Патрик, очень сложно расшифровать то, что вы просите.Пожалуйста, предоставьте некоторые фрагменты кода, чтобы показать, что вы получаете и чего надеетесь достичь.
Сказав это, я сделаю дикое предположение, что вы находитесь в ситуации, когда решатель равен unsat, т.е.(check-sat) возвращает ответ unsat.Тем не менее, ваш скрипт имеет (get-model) в следующей строке, что, конечно, приводит к ошибкам, так как нет модели.И вы хотели бы избежать сообщения об ошибке.
Это известное ограничение языка команд SMTLib: к сожалению, вы не можете программно проверять вывод команд.Обычный способ решить проблему такого рода - это иметь «живое» соединение с решателем (обычно в форме текстового канала), читать строку после выдачи (check-sat) и программно продолжать работу в зависимости от ответа.Так работает большинство систем, построенных на основе SMT-решателей.
Кроме того, вы можете использовать высокоуровневые API на других языках (C / C ++ / Java / Python / Haskell ..) и программировать z3 таким образом.;и использовать возможности языка хоста для управления этим взаимодействием.Это требует, чтобы вы изучили другой интерфейс поверх SMTLib, но для серьезных применений этой технологии вы, вероятно, не хотите ограничивать себя чисто интерфейсом SMTLib.
Также см. Этот ответ для соответствующего обсуждения.: Выполнение get-model или unsat-core в зависимости от решения решателя
Надеюсь, это решит вашу проблему, хотя из вашего вопроса трудно понять, к чему вы клонили.