diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 7124fd409..191e59a79 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -104,7 +104,7 @@ bool basics::basic_sign_lemma_model_based() {
                 return true;
         }
     }
-    return c().m_lemma_vec->size() > 0;
+    return c().m_lemmas.size() > 0;
 }
 
     
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 3ab89e012..4990a087c 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -808,7 +808,7 @@ void core::print_stats(std::ostream& out) {
         
 
 void core::clear() {
-    m_lemma_vec->clear();
+    m_lemmas.clear();
     m_literal_vec->clear();
 }
     
@@ -1045,7 +1045,7 @@ rational core::val(const factorization& f) const {
 }
 
 new_lemma::new_lemma(core& c, char const* name):name(name), c(c) {
-    c.m_lemma_vec->push_back(lemma());
+    c.m_lemmas.push_back(lemma());
 }
 
 new_lemma& new_lemma::operator|=(ineq const& ineq) {
@@ -1067,7 +1067,7 @@ new_lemma::~new_lemma() {
 }
 
 lemma& new_lemma::current() const {
-    return c.m_lemma_vec->back();
+    return c.m_lemmas.back();
 }
 
 new_lemma& new_lemma::operator&=(lp::explanation const& e) {
@@ -1180,7 +1180,7 @@ void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
 }
 
 bool core::conflict_found() const {
-    for (const auto & l : * m_lemma_vec) {
+    for (const auto & l : m_lemmas) {
         if (l.is_conflict())
             return true;
     }
@@ -1188,7 +1188,7 @@ bool core::conflict_found() const {
 }
 
 bool core::done() const {
-    return m_lemma_vec->size() >= 10 || 
+    return m_lemmas.size() >= 10 || 
         conflict_found() || 
         lp_settings().get_cancel_flag();
 }
@@ -1477,7 +1477,7 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
     for (unsigned i = 0; i < sz; ++i) 
         bound += checks[i].first;
     uint_set seen;
-    while (bound > 0 && !done() && m_lemma_vec->empty()) {
+    while (bound > 0 && !done() && m_lemmas.empty()) {
         unsigned n = random() % bound;
         for (unsigned i = 0; i < sz; ++i) {
             if (seen.contains(i))
@@ -1493,13 +1493,13 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
     }
 }
 
-lbool core::check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& l_vec) {
-    m_lemma_vec =  &l_vec;
-    return m_powers.check(r, x, y, l_vec);
+lbool core::check_power(lpvar r, lpvar x, lpvar y) {
+    m_lemmas.reset();
+    return m_powers.check(r, x, y, m_lemmas);
 }
 
-void core::check_bounded_divisions(vector<lemma>& l_vec) {
-    m_lemma_vec = &l_vec;
+void core::check_bounded_divisions() {
+    m_lemmas.reset();
     m_divisions.check_bounded_divisions();
 }
 // looking for a free variable inside of a monic to split
@@ -1518,11 +1518,10 @@ void core::add_bounds() {
     }    
 }
 
-lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
+lbool core::check(vector<ineq>& lits) {
     lp_settings().stats().m_nla_calls++;
     TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
     lra.get_rid_of_inf_eps();
-    m_lemma_vec =  &l_vec;
     m_literal_vec = &lits;
     if (!(lra.get_status() == lp::lp_status::OPTIMAL || 
           lra.get_status() == lp::lp_status::FEASIBLE)) {
@@ -1543,7 +1542,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
     bool run_bounded_nlsat = should_run_bounded_nlsat();
     bool run_bounds = params().arith_nl_branching();    
 
-    auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); };
+    auto no_effect = [&]() { return !done() && m_lemmas.empty() && lits.empty(); };
     
     if (no_effect())
         m_monomial_bounds.propagate();
@@ -1561,7 +1560,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
               {1, check2},
               {1, check3} };
         check_weighted(3, checks);
-        if (!l_vec.empty() || !lits.empty())
+        if (!m_lemmas.empty() || !lits.empty())
             return l_false;
     }
                 
@@ -1598,15 +1597,15 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
         m_stats.m_nra_calls++;
     }
     
-    if (ret == l_undef && !l_vec.empty() && m_reslim.inc()) 
+    if (ret == l_undef && !m_lemmas.empty() && m_reslim.inc()) 
         ret = l_false;
 
-    m_stats.m_nla_lemmas += l_vec.size();
-    for (const auto& l : l_vec)
+    m_stats.m_nla_lemmas += m_lemmas.size();
+    for (const auto& l : m_lemmas)
         m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size());
 
     
-    TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";);
+    TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
     IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
     CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monics(tout););
     return ret;
@@ -1641,13 +1640,13 @@ lbool core::bounded_nlsat() {
         m_nlsat_delay /= 2;
     }
     if (ret == l_true) {
-        m_lemma_vec->reset();
+        m_lemmas.reset();
     }
     return ret;
 }
 
 bool core::no_lemmas_hold() const {
-    for (auto & l : * m_lemma_vec) {
+    for (auto & l : m_lemmas) {
         if (lemma_holds(l)) {
             TRACE("nla_solver", print_lemma(l, tout););
             return false;
@@ -1656,10 +1655,10 @@ bool core::no_lemmas_hold() const {
     return true;
 }
     
-lbool core::test_check(vector<lemma>& l) {
+lbool core::test_check() {
     vector<ineq> lits;
     lra.set_status(lp::lp_status::OPTIMAL);
-    return check(lits, l);
+    return check(lits);
 }
 
 std::ostream& core::print_terms(std::ostream& out) const {
@@ -1811,12 +1810,11 @@ bool core::improve_bounds() {
     return bounds_improved;
 }
     
-void core::propagate(vector<lemma>& lemmas) {
+void core::propagate() {
     // disable for now
     return;
    // propagate linear monomials
-    lemmas.reset();
-    m_lemma_vec = &lemmas;
+    m_lemmas.reset();
  
     m_monomial_bounds.unit_propagate();
    
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 9c96f2fbf..b50e43b32 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -85,7 +85,7 @@ class core {
     reslimit&                m_reslim;
     smt_params_helper        m_params;
     std::function<bool(lpvar)> m_relevant;
-    vector<lemma> *          m_lemma_vec;
+    vector<lemma>            m_lemmas;
     vector<ineq> *           m_literal_vec = nullptr;
     indexed_uint_set                m_to_refine;
     tangents                 m_tangents;
@@ -386,15 +386,15 @@ public:
 
     bool  conflict_found() const;
     
-    lbool check(vector<ineq>& ineqs, vector<lemma>& l_vec);
-    lbool check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& l_vec);
-    void check_bounded_divisions(vector<lemma>&);
+    lbool check(vector<ineq>& ineqs);
+    lbool check_power(lpvar r, lpvar x, lpvar y);
+    void check_bounded_divisions();
 
     bool  no_lemmas_hold() const;
 
-    void propagate(vector<lemma>& lemmas);
+    void propagate();
     
-    lbool  test_check(vector<lemma>& l);
+    lbool  test_check();
     lpvar map_to_root(lpvar) const;
     std::ostream& print_terms(std::ostream&) const;
     std::ostream& print_term(const lp::lar_term&, std::ostream&) const;
@@ -428,6 +428,7 @@ public:
     void set_use_nra_model(bool m);
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
+    vector<nla::lemma> const& lemmas() const { return m_lemmas; } 
 private:
     void restore_patched_values();
     void constrain_nl_in_tableau();
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index b7197ff2f..5417d5d63 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -42,12 +42,12 @@ namespace nla {
     
     bool solver::need_check() { return m_core->has_relevant_monomial(); }
     
-    lbool solver::check(vector<ineq>& lits, vector<lemma>& lemmas) {
-        return m_core->check(lits, lemmas);
+    lbool solver::check(vector<ineq>& lits) {
+        return m_core->check(lits);
     }
 
-    void solver::propagate(vector<lemma>& lemmas) {
-        m_core->propagate(lemmas);
+    void solver::propagate() {
+        m_core->propagate();
     }
     
     void solver::push(){
@@ -93,12 +93,15 @@ namespace nla {
     }
 
     // ensure r = x^y, add abstraction/refinement lemmas
-    lbool solver::check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
-        return m_core->check_power(r, x, y, lemmas);
+    lbool solver::check_power(lpvar r, lpvar x, lpvar y) {
+        return m_core->check_power(r, x, y);
     }
 
-    void solver::check_bounded_divisions(vector<lemma>& lemmas) {
-        m_core->check_bounded_divisions(lemmas);
+    void solver::check_bounded_divisions() {
+        m_core->check_bounded_divisions();
     }
 
+    vector<nla::lemma> const& solver::lemmas() const {
+        return m_core->lemmas();
+    }
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 7a8a97b3f..9a1bf9d14 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -31,14 +31,14 @@ namespace nla {
         void add_idivision(lpvar q, lpvar x, lpvar y);
         void add_rdivision(lpvar q, lpvar x, lpvar y);
         void add_bounded_division(lpvar q, lpvar x, lpvar y);
-        void check_bounded_divisions(vector<lemma>&);
+        void check_bounded_divisions();
         void set_relevant(std::function<bool(lpvar)>& is_relevant);
         void push();
         void pop(unsigned scopes);
         bool need_check();
-        lbool check(vector<ineq>& lits, vector<lemma>&);
-        void propagate(vector<lemma>& lemmas);
-        lbool check_power(lpvar r, lpvar x, lpvar y, vector<lemma>&);
+        lbool check(vector<ineq>& lits);
+        void propagate();
+        lbool check_power(lpvar r, lpvar x, lpvar y);
         bool is_monic_var(lpvar) const;
         bool influences_nl_var(lpvar) const;
         std::ostream& display(std::ostream& out) const;
@@ -47,5 +47,6 @@ namespace nla {
         nlsat::anum_manager& am();
         nlsat::anum const& am_value(lp::var_index v) const;
         void collect_statistics(::statistics & st);
+        vector<nla::lemma> const& lemmas() const;
     };
 }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index c06b8fafb..4c6e5b4be 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1459,11 +1459,11 @@ namespace arith {
             return l_true;
 
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
+        lbool r = m_nla->check(m_nla_literals);
         switch (r) {
         case l_false:
             assume_literals();
-            for (const nla::lemma& l : m_nla_lemma_vector)
+            for (const nla::lemma& l : m_nla->lemmas())
                 false_case_of_check_nla(l);
             break;
         case l_true:
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index e23162393..f21e41786 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -248,7 +248,6 @@ namespace arith {
 
         // lemmas
         lp::explanation     m_explanation;
-        vector<nla::lemma>  m_nla_lemma_vector;
         vector<nla::ineq>   m_nla_literals;
         literal_vector      m_core, m_core2;
         vector<rational>    m_coeffs;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 41426e0d6..518cffe25 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1598,11 +1598,11 @@ public:
             return FC_DONE;
         if (!m_nla)
             return FC_GIVEUP;
-        switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y), m_nla_lemma_vector)) {
+        switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y))) {
         case l_true:
             return FC_DONE;
         case l_false:
-            for (const nla::lemma & l : m_nla_lemma_vector) 
+            for (const nla::lemma & l : m_nla->lemmas()) 
                 false_case_of_check_nla(l);
             return FC_CONTINUE;
         case l_undef:
@@ -1800,8 +1800,8 @@ public:
         if (!m_nla)
             return true;
         m_nla_lemma_vector.reset();
-        m_nla->check_bounded_divisions(m_nla_lemma_vector);
-        for (auto & lemma : m_nla_lemma_vector)
+        m_nla->check_bounded_divisions();
+        for (auto & lemma : m_nla->lemmas())
             false_case_of_check_nla(lemma);
         return m_nla_lemma_vector.empty();         
     }
@@ -2022,13 +2022,13 @@ public:
     
     final_check_status check_nla_continue() {
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
+        lbool r = m_nla->check(m_nla_literals);
 
         switch (r) {
         case l_false:
             for (const nla::ineq& i : m_nla_literals)
                 assume_literal(i); 
-            for (const nla::lemma & l : m_nla_lemma_vector) 
+            for (const nla::lemma & l : m_nla->lemmas()) 
                 false_case_of_check_nla(l);
             return FC_CONTINUE;
         case l_true:
@@ -2161,8 +2161,8 @@ public:
     void propagate_nla() {
         if (!m_nla)
             return;
-        m_nla->propagate(m_nla_lemma_vector);
-        for (nla::lemma const& l : m_nla_lemma_vector)
+        m_nla->propagate();
+        for (nla::lemma const& l : m_nla->lemmas())
             false_case_of_check_nla(l);
     }
 
diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp
index ce934e7ca..054c6583f 100644
--- a/src/test/lp/nla_solver_test.cpp
+++ b/src/test/lp/nla_solver_test.cpp
@@ -179,7 +179,6 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
     v.push_back(lp_a);v.push_back(lp_c);
     nla.add_monic(lp_ac, v.size(), v.begin());
      
-    vector<lemma> lv;
 
     // set abcde = ac * bde
     // ac = 1 then abcde = bde, but we have abcde < bde
@@ -193,8 +192,9 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
     s.set_column_value_test(lp_bde, lp::impq(rational(16)));
 
     
-    VERIFY(nla.get_core().test_check(lv) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
     
+    auto const& lv = nla.get_core().lemmas();
     nla.get_core().print_lemma(lv.back(), std::cout);
 
     ineq i0(lp_ac, llc::NE, 1);
@@ -250,8 +250,6 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
     svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
     nla.add_monic(lp_bde, v.size(), v.begin());
 
-    vector<lemma> lemma;
-
     s_set_column_value_test(s, lp_a, rational(1));
     s_set_column_value_test(s, lp_b, rational(1));
     s_set_column_value_test(s, lp_c, rational(1));
@@ -259,7 +257,8 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
     s_set_column_value_test(s, lp_e, rational(1));
     s_set_column_value_test(s, lp_bde, rational(3));
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     SASSERT(lemma[0].size() == 4);
     nla.get_core().print_lemma(lemma.back(), std::cout);
 
@@ -330,7 +329,6 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
                  lp_bde,
                  lp_acd,
                  lp_be);
-    vector<lemma> lemma;
 
     // set vars
     s_set_column_value_test(s, lp_a, rational(1));
@@ -344,7 +342,8 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
     s_set_column_value_test(s, lp_acd, rational(1));
     s_set_column_value_test(s, lp_be, rational(1));
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemma.back(), std::cout);
     SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
     lp::lar_term t0, t1;
@@ -389,14 +388,13 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
     vec.push_back(lp_d);
     nla.add_monic(lp_acd, vec.size(), vec.begin());
     
-    vector<lemma> lemma;
     s_set_column_value_test(s, lp_a, rational(1));
     s_set_column_value_test(s, lp_c, rational(1));
     s_set_column_value_test(s, lp_d, rational(1));
     s_set_column_value_test(s, lp_acd, rational(0));
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
-    
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemma.back(), std::cout);
 
     ineq i0(lp_a, llc::EQ, 0);
@@ -452,7 +450,6 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
                  lp_bde,
                  lp_acd,
                  lp_be);
-    vector<lemma> lemma;
 
     // set all vars to 1
     s_set_column_value_test(s, lp_a, rational(1));
@@ -471,8 +468,8 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
     s_set_column_value_test(s, lp_b, - rational(2));
     // we have bde = -b, therefore d = +-1 and e = +-1
     s_set_column_value_test(s, lp_d,  rational(3));
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
-
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     
     nla.get_core().print_lemma(lemma.back(), std::cout);
     ineq i0(lp_d, llc::EQ, 1);
@@ -584,9 +581,8 @@ void test_basic_sign_lemma() {
     s_set_column_value_test(s, lp_bde, rational(5));
     s_set_column_value_test(s, lp_acd, rational(3));
    
-    vector<lemma> lemmas;
-    VERIFY(nla.get_core().test_check(lemmas) == l_false);
-
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemmas = nla.get_core().lemmas();
     lp::lar_term t;
     t.add_var(lp_bde);
     t.add_var(lp_acd);
@@ -707,9 +703,9 @@ void test_order_lemma_params(bool var_equiv, int sign) {
         s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij)
                            + rational(1));
     }
-    vector<lemma> lemma;
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     // lp::lar_term t;
     // t.add_monomial(lp_bde);
     // t.add_monomial(lp_acd);
@@ -792,8 +788,8 @@ void test_monotone_lemma() {
     // set ef = ij while it has to be ef > ij
     s_set_column_value_test(s, lp_ef, s.get_column_value(lp_ij));
 
-    vector<lemma> lemma;
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemma.back(), std::cout);
     */
 }
@@ -821,8 +817,8 @@ void test_tangent_lemma_rat() {
     vec.push_back(lp_b);
     nla.add_monic(lp_ab, vec.size(), vec.begin());
     
-    vector<lemma> lemma;
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
+    VERIFY(nla.get_core().test_check() == l_false);
+    auto const& lemma = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemma.back(), std::cout);
 }
 
@@ -848,9 +844,8 @@ void test_tangent_lemma_reg() {
     vec.push_back(lp_b);
     nla.add_monic(lp_ab, vec.size(), vec.begin());
     
-    vector<lemma> lemma;
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
-    nla.get_core().print_lemma(lemma.back(), std::cout);
+    VERIFY(nla.get_core().test_check() == l_false);
+    nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
 }
 
 void test_tangent_lemma_equiv() {
@@ -893,10 +888,9 @@ void test_tangent_lemma_equiv() {
     int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
     
     s_set_column_value_test(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
-    vector<lemma> lemma;
 
-    VERIFY(nla.get_core().test_check(lemma) == l_false);
-    nla.get_core().print_lemma(lemma.back(), std::cout);
+    VERIFY(nla.get_core().test_check() == l_false);
+    nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
     */
 }