Z3, solver : smtlib2 : push (n = 1)에 정의 된대로 assertion-stack에 빈 레벨을 푸세요.

Question

현재 Python에서 Z3을 사용하고 있습니다. 레벨을 푸시하고 나중에 팝하는 어설 션 스택을 만들고 싶습니다. 푸시 및 팝 조작이있는 다른 "스택"과 똑같이 작동해야합니다. 따라서 SMTLIB2 표준은 선택적 숫자 n을 갖는 "push (n)"및 "pop (n)"의 두 가지 기능을 정의합니다. 내 경우 엔 항상 1이됩니다.

그러나 Z3에는 이상한 행동이있는 것 같습니다. 다음 코드로 인해 "인덱스가 범위를 벗어납니다"가 발생합니까?

s = Solver() 
s.push()  # expected: one new level on the stack, reality: emtpy stack 
s.pop(1)  # expected: stack is empty, reality: exception (index out of bounds) 

어설 션을 추가하면 Z3이 예상대로 작동합니다.

s = Solver() 
s.push() 
s.add(True) # now there is one level on the stack, 
s.pop(1)  # pop is successful 

심지어이 올바른 작동 : 많은 주장이 내 프로그램에서 만든 얼마나 많은 수준과 어떻게 모르는

s = Solver() 
s.add(True) 
s.push()  # now there is one level on the stack, 
s.pop(1)  # pop is successful 

문제는,. 어설 션이 전혀없고 단 한 수준 밖에 없다는 것은 가능합니다. 그런 다음 프로그램이 중단되거나 예외가 catch됩니다. 해결 방법은 첫 번째 단계로 항상 "참"과 같은 간단한 수식을 추가하는 것이지만 이것은 추한 것처럼 보입니다.

Z3에서 버그입니까? 아니면이 동작이 정확합니까?

Answer 1

이 버그는 unstable (작업중인 진행 중) 지점에서 수정되었습니다. 다음 공식 릴리스에서 사용할 수 있습니다. 그 동안 불안정한 지점을 컴파일하는 방법에 대한 지침은 here입니다. 수정본은 nightly buildscodeplex에서 사용할 수 있습니다.