Z3 범위에 레이블을 지정하고 특정 범위로 다시 표시

Question

Z3 범위에 레이블을 지정하고 (SMTLib2 구문) 특정 대상으로 다시 팝백 할 수 있습니까? 예를 들면 :

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

내가 (pop 2) 두 범위를 팝업 수 있다는 것을 알고 있지만, 내 시나리오에서이 내가 푸시 팝 쌍 사이에서 열 아직 닫히지 않은 범위의 수를 추적 할 필요가 있음을 의미해야 즉, (push foo) 이전의 Z3 컨텍스트를 복원해야합니다.

Answer 1

아니요, Z3은 명명 된 범위를 지원하지 않습니다.