Declare symbols that remain valid outside their sc

问题:

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?

回答1:

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.

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