貼標籤Z3範圍並彈出回到特定的一個

Question

是否可以標記Z3範圍（SMTLib2語法）然後回彈到特定的範圍？例如：

(push foo) 
    ; ... 
(push) 
    ; ... 
(pop foo) ; pops two scopes 

我知道，我可以彈出兩個作用域與(pop 2)，但在我的情況，這意味着我必須保持在推入 - 彈出對之間開通又未封閉的觀測器數的軌道必須匹配，也就是說，必須恢復在(push foo)之前存在的Z3上下文。

Answer 1

不，Z3不支持命名範圍。