diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 97deb47a6..b82bcfa8b 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2331,11 +2331,12 @@ public:
     }
 
     void operator()(expr_ref& fml, proof_ref& pr) {
-        if (!m.proofs_enabled()) {
-            expr_ref tmp(m);
-            m_elim_star(fml, tmp, pr);
-            fml = std::move(tmp);
+        expr_ref tmp(m);
+        m_elim_star(fml, tmp, pr);
+        if (m.proofs_enabled()) {
+            pr = m.mk_rewrite(fml, tmp);
         }
+        fml = std::move(tmp);
     }
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9a7fd1598..973394375 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3916,7 +3916,8 @@ public:
         if (!use_bounded_expansion())
             return;
         ctx().push_trail(value_trail<context, literal>(m_bounded_range_lit));
-        m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort());
+        if (!m_bound_predicate || !m_term2bound_info.empty())
+            m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort());
         m_bounded_range_lit = mk_literal(m_bound_predicate);
         // add max-unfolding literal
         // add variable bounds
@@ -3947,8 +3948,10 @@ public:
             else if (m_predicate2term.find(e, t)) {
                 found = true;
                 bound_info bi;
-                VERIFY(m_term2bound_info.find(t, bi));
-                if (bi.m_range >= max_range()) {
+                if (!m_term2bound_info.find(t, bi)) {
+                    TRACE("arith", tout << "bound information for term " << mk_pp(t, m) << " not found\n";);
+                }
+                else if (bi.m_range >= max_range()) {
                     m_term2bound_info.erase(t);
                 }
                 else {
@@ -3981,6 +3984,15 @@ public:
         m_term2bound_info.insert(t, bi);
     }
 
+    void setup() {
+        m_bounded_range_lit = null_literal;
+        m_bound_predicates.reset();
+        m_bound_predicate = nullptr;
+        m_predicate2term.reset();
+        m_term2bound_info.reset();
+    }
+
+
 };
     
 theory_lra::theory_lra(context& ctx):
@@ -4109,6 +4121,9 @@ void theory_lra::add_theory_assumptions(expr_ref_vector& assumptions) {
 bool theory_lra::should_research(expr_ref_vector& unsat_core) {
     return m_imp->should_research(unsat_core);
 }
+void theory_lra::setup() {
+    m_imp->setup();
+}
 
 }
 template  class lp::lp_bound_propagator<smt::theory_lra::imp>;
diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h
index 128b3eb0d..041a930ee 100644
--- a/src/smt/theory_lra.h
+++ b/src/smt/theory_lra.h
@@ -95,6 +95,8 @@ namespace smt {
         
         void collect_statistics(::statistics & st) const override;
 
+        void setup() override;
+
         void add_theory_assumptions(expr_ref_vector& assumptions) override;
 
         bool should_research(expr_ref_vector& unsat_core) override;