У меня проблемы с выяснением, как отлаживать z3. Есть ли способ узнать, что движок SMT «пытается» облегчить, чтобы понять, почему он не видит решение, которое кажется очевидным и куда вместо этого он посвящает свое время?
В качестве примера в моем конкретном случае я работаю с рекурсивной функцией и устанавливаю z3, чтобы найти входы, в которых функция имеет определенный результат. SMT истекает, у yadda yadda yadda оказывается, что у вещи, на которой я повторяюсь, был базовый случай 0, но если он когда-нибудь станет отрицательным, он будет повторяться вечно. Z3 не знал, чтобы не выбрать отрицательное число, поэтому он застрянет. Я понял это, взглянув на код, но если бы у меня был какой-то вывод, в котором было написано: «пробуя i == -10, пробуя i == -11 и т. Д.», Было бы совершенно очевидно, что происходит неправильно.
У меня продолжают возникать менее очевидные проблемы, и я подозреваю, что Z3 все еще застревает в циклах. Как я могу увидеть петлю, в которой она застревает?