У меня есть некоторый код в IR, и этот код уже находится в форме SSA. Сейчас я пытаюсь преобразовать этот код в формулу SMT, а затем передать его в Z3, чтобы выполнить некоторую проверку. У меня есть несколько вопросов:

Есть ли технический документ, в котором подробно объясняется, как преобразовать SSA IR в формулу SMT? Я искал вокруг, но безрезультатно.

Для этих вычислительных инструкций нет особых проблем с преобразованием в формулу Z3. Тем не менее, я все еще борюсь с безусловными и условными инструкциями ветвления. Любое предложение о том, как преобразовать эти инструкции в формулу Z3?

Спасибо!!!