Popping that assertion level removes them. As an alternative, declarations and definitions can all be made global by running the solver with the option :global-declarations set to true. When running with this option set, all declarations and definitions become permanent. That is, they survive any pop operations on the assertion stack as well as invocations of reset-assertions and can only be removed by a global reset, achieved with the reset command.
The following example fails :
(set-logic ALL)
(set-option :global-declarations)
(push 1)
(declare-const x Int)
(pop 1)
(assert (= x x))
with the error Unbound identifier x. Same goes with the following example :
(set-logic ALL)
(set-option :global-declarations)
(declare-const x Int)
(reset-assertions)
(assert (= x x))
The SMT standard states (https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf#page=56) :
The following example fails :
with the error
Unbound identifier x. Same goes with the following example :