Можно ли маркировать области действия Z3 (синтаксис SMTLib2) и затем возвращаться к определенной?Например:
(push foo)
; ...
(push)
; ...
(pop foo) ; pops two scopes
Я знаю, что могу выдвинуть две области с помощью (pop 2), но в моем сценарии это означает, что я должен отслеживать количество еще не открытых областей, открытых между нажатиемпоп-пара, которая должна совпадать, то есть должна восстанавливать контекст Z3, существовавший до (push foo).