Z3 2.x 具有符号声明没有弹出的特性(好吧,可能是错误),例如 Z3 2.x 接受以下代码:
(push)
(declare-fun x () Int)
; Assumptions made in this scope will be popped correctly
(pop)
(assert (= x x))
Z3 3.x 不再接受此代码(“未知常量”)。
有没有办法恢复旧的行为?或者另一种方式,如何在范围内声明符号,使得声明(并且只有声明,而不是假设)是全局的,即不弹出?
Z3 2.x 具有符号声明没有弹出的特性(好吧,可能是错误),例如 Z3 2.x 接受以下代码:
(push)
(declare-fun x () Int)
; Assumptions made in this scope will be popped correctly
(pop)
(assert (= x x))
Z3 3.x 不再接受此代码(“未知常量”)。
有没有办法恢复旧的行为?或者另一种方式,如何在范围内声明符号,使得声明(并且只有声明,而不是假设)是全局的,即不弹出?