diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index dd910446e..a075f3072 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -35,6 +35,7 @@ Revision History:
 #include "smt/smt_model_generator.h"
 #include "smt/arith_eq_adapter.h"
 #include "util/nat_set.h"
+#include "util/lp/nra_solver.h"
 #include "tactic/filter_model_converter.h"
 
 namespace lp {
@@ -144,10 +145,10 @@ namespace smt {
         ast_manager&         m;
         theory_arith_params& m_arith_params;
         arith_util           a;
-
         arith_eq_adapter     m_arith_eq_adapter;
+        vector<rational>     m_columns;
+      
 
-        vector<rational>    m_columns;
         // temporary values kept during internalization
         struct internalize_state {
             expr_ref_vector     m_terms;                     
@@ -248,6 +249,8 @@ namespace smt {
 
         unsigned               m_num_conflicts;
 
+        scoped_ptr<nra::solver> m_nra;
+        bool                    m_use_nra_model;
 
         struct var_value_eq {
             imp & m_th;
@@ -291,6 +294,16 @@ namespace smt {
             //m_solver->settings().set_ostream(0);
         }
 
+        void ensure_nra() {
+            if (!m_nra) {
+                m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params());
+                for (unsigned i = 0; i < m_scopes.size(); ++i) {
+                    m_nra->push();
+                }
+            }
+        }
+
+
         void found_not_handled(expr* n) {
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
@@ -456,7 +469,8 @@ namespace smt {
             }
             TRACE("arith", tout << mk_pp(t, m) << "\n";);
             if (!_has_var) {
-                m_solver->add_monomial(get_var_index(v), vars);
+                ensure_nra();
+                m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
             }
         }
 
@@ -711,7 +725,8 @@ namespace smt {
             m_num_conflicts(0),
             m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
             m_solver(0),
-            m_resource_limit(*this) {
+            m_resource_limit(*this),
+            m_use_nra_model(false) {
         }
         
         ~imp() {
@@ -868,6 +883,7 @@ namespace smt {
             s.m_underspecified_lim = m_underspecified.size();
             s.m_var_trail_lim = m_var_trail.size();
             if (!m_delay_constraints) m_solver->push();
+            if (m_nra) m_nra->push();
         }
 
         void pop_scope_eh(unsigned num_scopes) {
@@ -900,6 +916,7 @@ namespace smt {
             // VERIFY(l_false != make_feasible());
             m_new_bounds.reset();
             m_to_check.reset();
+            if (m_nra) m_nra->pop(num_scopes);
             TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
         }
 
@@ -1272,21 +1289,23 @@ namespace smt {
         }
 
         lbool check_nra() {
+            m_use_nra_model = false;
             if (m.canceled()) return l_undef;
-            // return l_true;
-            // TBD:
-            switch (m_solver->check_nra(m_variable_values, m_explanation)) {
-            case lean::final_check_status::DONE:
-                return l_true;
-            case lean::final_check_status::CONTINUE:
-                return l_true; // ?? why have a continue at this level ??
-            case lean::final_check_status::UNSAT: 
+            if (!m_nra) return l_true;
+            if (!m_nra->need_check()) return l_true;
+            lbool r = m_nra->check(m_explanation);
+            switch (r) {
+            case l_false:
                 set_conflict1();
-                return l_false;
-            case lean::final_check_status::GIVEUP:
-                return l_undef;
+                break;
+            case l_true:
+                m_use_nra_model = true;
+                // TBD: check equalities
+                break;
+            default:
+                break;
             }
-            return l_true;
+            return r;
         }
 
         /**
@@ -2355,9 +2374,16 @@ namespace smt {
         model_value_proc * mk_value(enode * n, model_generator & mg) {
             theory_var v = n->get_th_var(get_id());
             expr* o = n->get_owner();
-            rational r = get_value(v);
-            if (a.is_int(o) && !r.is_int()) r = floor(r);
-            return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
+            if (m_use_nra_model) {
+                SASSERT(m_nra);
+                app* e = a.mk_numeral(m_nra->value(m_theory_var2var_index[v]), a.is_int(o));
+                return alloc(expr_wrapper_proc, e);
+            }
+            else {
+                rational r = get_value(v);
+                if (a.is_int(o) && !r.is_int()) r = floor(r);
+                return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
+            }
         }
 
         bool get_value(enode* n, expr_ref& r) {
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index b3da4e8ba..882ce229e 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -32,7 +32,6 @@ lar_solver::lar_solver() : m_status(OPTIMAL),
                            m_terms_start_index(1000000),
                            m_mpq_lar_core_solver(m_settings, *this)
 {
-    m_nra = alloc(nra::solver, *this);
 }
     
 void lar_solver::set_propagate_bounds_on_pivoted_rows_mode(bool v) {
@@ -332,7 +331,6 @@ void lar_solver::push() {
     m_term_count.push();
     m_constraint_count = m_constraints.size();
     m_constraint_count.push();
-    m_nra->push();
 }
 
 void lar_solver::clean_large_elements_after_pop(unsigned n, int_set& set) {
@@ -388,7 +386,6 @@ void lar_solver::pop(unsigned k) {
     m_settings.simplex_strategy() = m_simplex_strategy;
     lean_assert(sizes_are_correct());
     lean_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
-    m_nra->pop(k);
 }
     
 vector<constraint_index> lar_solver::get_all_constraint_indices() const {
@@ -1088,13 +1085,6 @@ void lar_solver::get_infeasibility_explanation(vector<std::pair<mpq, constraint_
     lean_assert(explanation_is_correct(explanation));
 }
 
-final_check_status lar_solver::check_nra(nra_model_t& model, explanation_t& explanation) {
-    return m_nra->check(model, explanation);
-}
-
-void lar_solver::add_monomial(var_index v, svector<var_index> const& vars) {
-    m_nra->add_monomial(v, vars.size(), vars.c_ptr());
-}
 
 
 void lar_solver::get_infeasibility_explanation_for_inf_sign(
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 6937455ae..b8c5ce608 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -31,7 +31,6 @@
 #include "util/lp/quick_xplain.h"
 #include "util/lp/conversion_helper.h"
 #include "util/lp/int_solver.h"
-#include "util/lp/nra_solver.h"
 
 namespace lean {
 
@@ -64,7 +63,6 @@ class lar_solver : public column_namer {
     vector<lar_term*> m_terms;
     const var_index m_terms_start_index;
     indexed_vector<mpq> m_column_buffer;
-    scoped_ptr<nra::solver> m_nra;
 public:
     lar_core_solver m_mpq_lar_core_solver;
     unsigned constraint_count() const;
@@ -204,8 +202,6 @@ public:
 
     lp_status find_feasible_solution();
    
-    final_check_status check_nra(nra_model_t& model, explanation_t& explanation);    
-
     void add_monomial(var_index v, svector<var_index> const& vars);
     
     lp_status solve();
diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h
index f07fbeef7..3f082ab10 100644
--- a/src/util/lp/lp_settings.h
+++ b/src/util/lp/lp_settings.h
@@ -26,8 +26,6 @@ enum class final_check_status {
 
 typedef vector<std::pair<mpq, constraint_index>> explanation_t;
 
-typedef std::unordered_map<lean::var_index, rational> nra_model_t;
-
 
 enum class column_type  {
     free_column = 0,
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index 5157be92c..695066048 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -16,9 +16,10 @@ namespace nra {
 
     struct solver::imp {
         lean::lar_solver& s;
-        reslimit      m_limit;  // TBD: extract from lar_solver
-        params_ref    m_params; // TBD: pass from outside
+        reslimit&      m_limit;  // TBD: extract from lar_solver
+        params_ref     m_params; // TBD: pass from outside
         u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables
+        nlsat::solver m_nlsat;
 
         struct mon_eq {
             mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs):
@@ -31,23 +32,15 @@ namespace nra {
         unsigned_vector                  m_lim;
         mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
 
-        imp(lean::lar_solver& s): 
-            s(s) {
+        imp(lean::lar_solver& s, reslimit& lim, params_ref const& p): 
+            s(s), 
+            m_limit(lim),
+            m_params(p),
+            m_nlsat(m_limit, m_params) {
         }
 
-        lean::final_check_status check_feasible(lean::nra_model_t& m, lean::explanation_t& ex) {
-            if (m_monomials.empty()) {
-                return lean::final_check_status::DONE;
-            }
-            if (check_assignments()) {
-                return lean::final_check_status::DONE;
-            }
-            switch (check_nlsat(m, ex)) {
-            case l_undef: return lean::final_check_status::GIVEUP;
-            case l_true: return lean::final_check_status::DONE;
-            case l_false: return lean::final_check_status::UNSAT;
-            }
-            return lean::final_check_status::DONE;
+        bool need_check() {
+            return !m_monomials.empty() && !check_assignments();
         }
 
         void add(lean::var_index v, unsigned sz, lean::var_index const* vs) {
@@ -97,71 +90,51 @@ namespace nra {
            
            TBD: use partial model from lra_solver to prime the state of nlsat_solver.
         */
-        lbool check_nlsat(lean::nra_model_t& model, lean::explanation_t& ex) {
-            nlsat::solver solver(m_limit, m_params);
+        lbool check(lean::explanation_t& ex) {
+            SASSERT(need_check());
+            m_nlsat.reset();
             m_lp2nl.reset();
+            vector<nlsat::assumption, false> core;
+
             // add linear inequalities from lra_solver
             for (unsigned i = 0; i < s.constraint_count(); ++i) {
-                add_constraint(solver, i);
+                add_constraint(i);
             }
 
             // add polynomial definitions.
             for (auto const& m : m_monomials) {
-                add_monomial_eq(solver, m);
+                add_monomial_eq(m);
             }
             // TBD: add variable bounds?
 
-
-            lbool r = solver.check(); 
-            TRACE("arith", solver.display(tout << r << "\n"););
+            lbool r = m_nlsat.check(); 
+            TRACE("arith", m_nlsat.display(tout << r << "\n"););
             switch (r) {
-            case l_true: {
-                nlsat::anum_manager& am = solver.am();
-                model.clear();
-                for (auto kv : m_lp2nl) {
-                    kv.m_key;
-                    nlsat::anum const& v = solver.value(kv.m_value);
-                    if (is_int(kv.m_key) && !am.is_int(v)) {
-                        // the nlsat solver should already have returned unknown.
-                        TRACE("lp", tout << "Value is not integer " << kv.m_key << "\n";);
-                        return l_undef;
-                    }
-                    if (!am.is_rational(v)) {
-                        // TBD extract and convert model.
-                        TRACE("lp", tout << "Cannot handle algebraic numbers\n";);
-                        return l_undef;
-                    }
-                    rational r;
-                    am.to_rational(v, r);
-                    model[kv.m_key] = r;
-                }
+            case l_true: 
                 break;
-            }
-            case l_false: {
+            case l_false: 
                 ex.reset();
-                vector<nlsat::assumption, false> core;
-                solver.get_core(core);
+                m_nlsat.get_core(core);
                 for (auto c : core) {
                     unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
                     ex.push_back(std::pair<rational, unsigned>(rational(1), idx));
                     TRACE("arith", tout << "ex: " << idx << "\n";);
                 }
                 break;
-            }
             case l_undef:
                 break;
             }            
             return r;
         }                
 
-        void add_monomial_eq(nlsat::solver& solver, mon_eq const& m) {
-            polynomial::manager& pm = solver.pm();
+        void add_monomial_eq(mon_eq const& m) {
+            polynomial::manager& pm = m_nlsat.pm();
             svector<polynomial::var> vars;
             for (auto v : m.m_vs) {
-                vars.push_back(lp2nl(solver, v));
+                vars.push_back(lp2nl(v));
             }
             polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
-            polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(solver, m.m_v), 1), pm);
+            polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.m_v), 1), pm);
             polynomial::monomial* mls[2] = { m1, m2 };
             polynomial::scoped_numeral_vector coeffs(pm.m());
             coeffs.push_back(mpz(1));
@@ -169,13 +142,13 @@ namespace nra {
             polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.c_ptr(), mls),  pm);
             polynomial::polynomial* ps[1] = { p };
             bool even[1] = { false };
-            nlsat::literal lit = solver.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
-            solver.mk_clause(1, &lit, 0);
+            nlsat::literal lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
+            m_nlsat.mk_clause(1, &lit, 0);
         }
 
-        void add_constraint(nlsat::solver& solver, unsigned idx) {
+        void add_constraint(unsigned idx) {
             auto& c = s.get_constraint(idx);
-            auto& pm = solver.pm();
+            auto& pm = m_nlsat.pm();
             auto k = c.m_kind;
             auto rhs = c.m_right_side;
             auto lhs = c.get_left_side_coefficients();
@@ -183,7 +156,7 @@ namespace nra {
             svector<polynomial::var> vars;
             rational den = denominator(rhs);
             for (auto kv : lhs) {
-                vars.push_back(lp2nl(solver, kv.second));
+                vars.push_back(lp2nl(kv.second));
                 den = lcm(den, denominator(kv.first));
             }
             vector<rational> coeffs;
@@ -197,24 +170,24 @@ namespace nra {
             nlsat::literal lit;
             switch (k) {
             case lean::lconstraint_kind::LE:
-                lit = ~solver.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
+                lit = ~m_nlsat.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
                 break;
             case lean::lconstraint_kind::GE:
-                lit = ~solver.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
+                lit = ~m_nlsat.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
                 break;
             case lean::lconstraint_kind::LT:
-                lit = solver.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
+                lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
                 break;
             case lean::lconstraint_kind::GT:
-                lit = solver.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
+                lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
                 break;
             case lean::lconstraint_kind::EQ:
-                lit = solver.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
+                lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
                 break;
             }
 
             nlsat::assumption a = this + idx;
-            solver.mk_clause(1, &lit, a);
+            m_nlsat.mk_clause(1, &lit, a);
         }               
 
         bool is_int(lean::var_index v) {
@@ -222,15 +195,20 @@ namespace nra {
             return false;
         }
 
-        polynomial::var lp2nl(nlsat::solver& solver, lean::var_index v) {
+
+        polynomial::var lp2nl(lean::var_index v) {
             polynomial::var r;
             if (!m_lp2nl.find(v, r)) {
-                r = solver.mk_var(is_int(v));
+                r = m_nlsat.mk_var(is_int(v));
                 m_lp2nl.insert(v, r);
             }
             return r;
         }
 
+        nlsat::anum const& value(lean::var_index v) const {
+           return m_nlsat.value(m_lp2nl.find(v));
+        }
+
         std::ostream& display(std::ostream& out) const {
             for (auto m : m_monomials) {
                 out << "v" << m.m_v << " = ";
@@ -244,8 +222,8 @@ namespace nra {
 
     };
 
-    solver::solver(lean::lar_solver& s) {
-        m_imp = alloc(imp, s);
+    solver::solver(lean::lar_solver& s, reslimit& lim, params_ref const& p) {
+        m_imp = alloc(imp, s, lim, p);
     }
 
     solver::~solver() {
@@ -256,8 +234,12 @@ namespace nra {
         m_imp->add(v, sz, vs);
     }
 
-    lean::final_check_status solver::check(lean::nra_model_t& m, lean::explanation_t& ex) {
-        return m_imp->check_feasible(m, ex);
+    lbool solver::check(lean::explanation_t& ex) {
+        return m_imp->check(ex);
+    }
+
+    bool solver::need_check() {
+        return m_imp->need_check();
     }
 
     void solver::push() {
@@ -272,4 +254,8 @@ namespace nra {
         return m_imp->display(out);
     }
 
+    nlsat::anum const& solver::value(lean::var_index v) const {
+        return m_imp->value(v);
+    }
+
 }
diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h
index 2fdf91729..4bd7a64a0 100644
--- a/src/util/lp/nra_solver.h
+++ b/src/util/lp/nra_solver.h
@@ -6,20 +6,26 @@
 #pragma once
 #include "util/vector.h"
 #include "util/lp/lp_settings.h"
+#include "util/rlimit.h"
+#include "util/params.h"
+#include "nlsat/nlsat_solver.h"
 
 namespace lean {
     class lar_solver;
 }
 
+
 namespace nra {
 
+    typedef std::unordered_map<lean::var_index, rational> nra_model_t;
+
     class solver {
         struct imp;
         imp* m_imp;
 
     public:
 
-        solver(lean::lar_solver& s);
+        solver(lean::lar_solver& s, reslimit& lim, params_ref const& p = params_ref());
         
         ~solver();
 
@@ -33,7 +39,17 @@ namespace nra {
           \brief Check feasiblity of linear constraints augmented by polynomial definitions
           that are added.
          */
-        lean::final_check_status check(lean::nra_model_t& m, lean::explanation_t& ex);
+        lbool check(lean::explanation_t& ex);
+
+        /*
+          \brief determine whether nra check is needed.
+        */
+        bool need_check();
+
+        /*
+          \brief Access model.
+        */
+        nlsat::anum const& value(lean::var_index v) const;
 
         /*
           \brief push and pop scope. 
@@ -47,5 +63,6 @@ namespace nra {
           \brief display state
          */
         std::ostream& display(std::ostream& out) const;
+
     };
 }