В Z3 2.x была особенность (ну, скорее, ошибка), что объявления символов не выскакивали, например. следующий код принимается Z3 2.x:
(push)
(declare-fun x () Int)
; Assumptions made in this scope will be popped correctly
(pop)
(assert (= x x))
Z3 3.x больше не принимает этот код ("неизвестная константа").
Есть ли способ восстановить старое поведение? Или, по-другому, как можно объявить символы внутри областей видимости, чтобы объявление (и только объявление, а не предположения) было глобальным, т. е. не всплывающим?
