目前我正在将 Z3 与 Python 一起使用。我想创建一个断言堆栈，我可以在其中推送一个级别并稍后弹出它。它应该与任何其他带有推送和弹出操作的“堆栈”一样工作。因此，SMTLIB2 标准定义了两个函数“push(n)”和“pop(n)”，可选数字为 n。在我的情况下，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
问题是，我不知道在我的程序中创建了多少级别和多少断言。有可能根本没有断言，只有一个级别。然后程序会崩溃（或捕获异常）。一种解决方法是添加一些简单的公式，如“True”总是作为第一步，但这看起来很难看。
这是 Z3 中的错误还是这种行为正确？