Labeling Z3 scopes and popping back to a specific one

Is it possible to labe开发者_运维百科l Z3 scopes (SMTLib2 syntax) and to then pop back to a specific one? For example:

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

I know that I can pop two scopes with (pop 2), but in my scenario this means that I have to keep track of the number of yet unclosed scopes opened in between a push-pop pair that must match, i.e. that must restore the Z3 context as it existed before (push foo).

---

No, Z3 does not have support for named scopes.