声明在其范围之外仍然有效的符号
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 had the feature (well, probably rather the bug) that symbol declarations were not popped away, e.g. the following code is accepted by Z3 2.x:
(push)
(declare-fun x () Int)
; Assumptions made in this scope will be popped correctly
(pop)
(assert (= x x))
Z3 3.x no longer accepts this code ("unknown constant").
Is there a way to restore the old behaviour? Or another way how one could declare symbols inside scopes such that the declaration (and only the declaration, not the assumptions) is global, i.e. not popped?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
是的，在 Z3 2.x 中所有声明都是全局的。我们在 Z3 3.x 中更改了此行为，因为 SMT-LIB 2.0 标准规定所有声明都应限定范围。
您可以使用选项
:global-decls恢复旧的行为。Yes, in Z3 2.x all declarations were global. We changed this behavior in Z3 3.x because the SMT-LIB 2.0 standard states that all declarations should be scoped.
You can restore the old behavior using the option
:global-decls.