Z3スコープ（SMTLib2構文）にラベルを付けてから、特定のスコープにポップバックすることは可能ですか？例えば：
(push foo)
; ...
(push)
; ...
(pop foo) ; pops two scopes
で2つのスコープをポップできることは知っています(pop 2)が、私のシナリオでは、これは、一致する必要があるプッシュポップペアの間に開いているまだ閉じられていないスコープの数を追跡する必要があることを意味します。つまり、Z3コンテキストを復元する必要があります。以前に存在していました(push foo)。