scope - 标记 Z3 范围并返回到特定范围

Question

是否可以标记 Z3 范围（SMTLib2 语法）然后弹回特定范围？例如：

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

我知道我可以使用 弹出两个范围(pop 2)，但在我的场景中，这意味着我必须跟踪在必须匹配的推-弹出对之间打开的尚未关闭的范围的数量，即必须恢复 Z3 上下文以前存在过(push foo)。

Answer 1

不，Z3 不支持命名范围。