声明在其范围外仍然有效的符号

Question

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不再接受此代码（“未知常量”）。

有没有办法恢复旧的行为？或者，另一种方式是如何在范围内声明符号，使得声明（以及只有声明，而不是假设）是全局的，即没有弹出？

Answer 1

是的，在Z3 2.x中所有的声明都是全局的。我们在Z3 3.x中改变了这种行为，因为SMT-LIB 2.0标准规定所有声明都应该被限定范围。 您可以使用选项:global-decls恢复旧行为。

(set-option :global-decls true) 
(push) 
(declare-fun x() Int) 
(pop) 
(assert (= x x))