diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 7707ba023..03850941d 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -24,6 +24,8 @@
 #include "math/lp/horner.h"
 #include "math/lp/nla_intervals.h"
 #include "math/grobner/pdd_solver.h"
+#include "math/lp/nla_lemma.h"
+#include "nlsat/nlsat_solver.h"
 
 
 namespace nla {
@@ -66,18 +68,6 @@ public:
     const rational& rs() const { return m_rs; };
 };
 
-class lemma {
-    vector<ineq>     m_ineqs;
-    lp::explanation  m_expl;
-public:
-    void push_back(const ineq& i) { m_ineqs.push_back(i);}
-    size_t size() const { return m_ineqs.size() + m_expl.size(); }
-    const vector<ineq>& ineqs() const { return m_ineqs; }
-    vector<ineq>& ineqs() { return m_ineqs; }
-    lp::explanation& expl() { return m_expl; }
-    const lp::explanation& expl() const { return m_expl; }
-    bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
-};
 
 class core;
 //
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 3c46c7897..19f27734f 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -12,8 +12,12 @@
 #include "math/lp/var_eqs.h"
 #include "math/lp/factorization.h"
 #include "math/lp/nla_solver.h"
+#include "math/lp/nla_core.h"
+
 namespace nla {
 
+nla_settings& solver::settings() { return m_core->m_nla_settings; }
+
 void solver::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
     m_core->add_monic(v, sz, vs);
 }
@@ -36,7 +40,8 @@ void solver::pop(unsigned n) {
     m_core->pop(n);
 }
         
-solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit))  {
+solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)),
+                                   m_nra(s, m_res_limit, *m_core) {
 }
 
 bool solver::influences_nl_var(lpvar j) const {    
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 7520c3fe0..63182731b 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -11,23 +11,27 @@ Author:
 #include "math/lp/lp_settings.h"
 #include "util/rlimit.h"
 #include "util/params.h"
-#include "nlsat/nlsat_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/monic.h"
-#include "math/lp/nla_core.h"
+#include "math/lp/nla_settings.h"
+#include "math/lp/nla_lemma.h"
 
+namespace nra {
+class solver;
+}
 namespace nla {
-
+class core;
 // nonlinear integer incremental linear solver
 class solver {
     reslimit m_res_limit;
     core* m_core;
+    nra::solver m_nra;
 public:
     void add_monic(lpvar v, unsigned sz, lpvar const* vs);
     
     solver(lp::lar_solver& s);
     ~solver();
-    nla_settings& settings() { return m_core->m_nla_settings; }
+    nla_settings& settings();
     void push();
     void pop(unsigned scopes);
     bool need_check();
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 7588231e6..732d21776 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -9,272 +9,273 @@
 #include "math/polynomial/polynomial.h"
 #include "math/polynomial/algebraic_numbers.h"
 #include "util/map.h"
-#include "math/lp/monic.h"
+#include "math/lp/nla_core.h"
+
 
 namespace nra {
 
 typedef nla::mon_eq mon_eq;
 
 typedef nla::variable_map_type variable_map_type;
-    struct solver::imp {
-        lp::lar_solver&      s;
-        reslimit&              m_limit;  
-        params_ref             m_params; 
-        u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables        
-        scoped_ptr<nlsat::solver> m_nlsat;
-        scoped_ptr<scoped_anum>   m_zero;
-        vector<mon_eq>            m_monics;
-        unsigned_vector           m_monics_lim;
-        mutable variable_map_type m_variable_values; // current model        
+struct solver::imp {
+    lp::lar_solver&      s;
+    reslimit&              m_limit;  
+    params_ref             m_params; 
+    u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables        
+    scoped_ptr<nlsat::solver> m_nlsat;
+    scoped_ptr<scoped_anum>   m_zero;
+    vector<mon_eq>            m_monics;
+    unsigned_vector           m_monics_lim;
+    mutable variable_map_type m_variable_values; // current model        
+    nla::core&                m_nla_core;    
+    imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core): 
+        s(s), 
+        m_limit(lim),
+        m_params(p),
+        m_nla_core(nla_core) {}
 
-        imp(lp::lar_solver& s, reslimit& lim, params_ref const& p): 
-            s(s), 
-            m_limit(lim),
-            m_params(p) {
-        }
+    bool need_check() {
+        return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values);
+    }
 
-        bool need_check() {
-            return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values);
-        }
+    void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
+        m_monics.push_back(mon_eq(v, sz, vs));
+    }
 
-        void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
-            m_monics.push_back(mon_eq(v, sz, vs));
-        }
+    void push() {
+        m_monics_lim.push_back(m_monics.size());
+    }
 
-        void push() {
-            m_monics_lim.push_back(m_monics.size());
-        }
+    void pop(unsigned n) {
+        if (n == 0) return;
+        m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]);
+        m_monics_lim.shrink(m_monics_lim.size() - n);       
+    }
 
-        void pop(unsigned n) {
-            if (n == 0) return;
-            m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]);
-            m_monics_lim.shrink(m_monics_lim.size() - n);       
-        }
+    /*
+      \brief Check if polynomials are well defined.
+      multiply values for vs and check if they are equal to value for v.
+      epsilon has been computed.
+    */
+    /*        bool check_assignment(mon_eq const& m) const {
+              rational r1 = m_variable_values[m.m_v];
+              rational r2(1);
+              for (auto w : m.vars()) {
+              r2 *= m_variable_values[w];
+              }
+              return r1 == r2;
+              }
 
-        /*
-          \brief Check if polynomials are well defined.
-          multiply values for vs and check if they are equal to value for v.
-          epsilon has been computed.
-        */
-        /*        bool check_assignment(mon_eq const& m) const {
-            rational r1 = m_variable_values[m.m_v];
-            rational r2(1);
-            for (auto w : m.vars()) {
-                r2 *= m_variable_values[w];
-            }
-            return r1 == r2;
-        }
-
-        bool check_assignments() const {
-            s.get_model(m_variable_values);
-            for (auto const& m : m_monics) {
-                if (!check_assignment(m)) return false;
-            }
-            return true;
-        }
-        */
-        /**
-           \brief one-shot nlsat check.
-           A one shot checker is the least functionality that can 
-           enable non-linear reasoning. 
-           In addition to checking satisfiability we would also need
-           to identify equalities in the model that should be assumed
-           with the remaining solver.
+              bool check_assignments() const {
+              s.get_model(m_variable_values);
+              for (auto const& m : m_monics) {
+              if (!check_assignment(m)) return false;
+              }
+              return true;
+              }
+    */
+    /**
+       \brief one-shot nlsat check.
+       A one shot checker is the least functionality that can 
+       enable non-linear reasoning. 
+       In addition to checking satisfiability we would also need
+       to identify equalities in the model that should be assumed
+       with the remaining solver.
            
-           TBD: use partial model from lra_solver to prime the state of nlsat_solver.
-           TBD: explore more incremental ways of applying nlsat (using assumptions)
-        */
-        lbool check(lp::explanation& ex) {
-            SASSERT(need_check());
-            m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
-            m_zero = alloc(scoped_anum, am());
-            m_lp2nl.reset();
-            vector<nlsat::assumption, false> core;
+       TBD: use partial model from lra_solver to prime the state of nlsat_solver.
+       TBD: explore more incremental ways of applying nlsat (using assumptions)
+    */
+    lbool check(lp::explanation& ex) {
+        SASSERT(need_check());
+        m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
+        m_zero = alloc(scoped_anum, am());
+        m_lp2nl.reset();
+        vector<nlsat::assumption, false> core;
 
-            // add linear inequalities from lra_solver
-            for (lp::constraint_index ci : s.constraints().indices()) {
-                add_constraint(ci);
+        // add linear inequalities from lra_solver
+        for (lp::constraint_index ci : s.constraints().indices()) {
+            add_constraint(ci);
+        }
+
+        // add polynomial definitions.
+        for (auto const& m : m_monics) {
+            add_monic_eq(m);
+        }
+        // TBD: add variable bounds?
+
+        lbool r = l_undef;
+        try {
+            r = m_nlsat->check(); 
+        }
+        catch (z3_exception&) {
+            if (m_limit.get_cancel_flag()) {
+                r = l_undef;
             }
-
-            // add polynomial definitions.
-            for (auto const& m : m_monics) {
-                add_monic_eq(m);
+            else {
+                throw;
             }
-            // TBD: add variable bounds?
-
-            lbool r = l_undef;
-            try {
-                r = m_nlsat->check(); 
+        }
+        TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
+        switch (r) {
+        case l_true: 
+            break;
+        case l_false: 
+            ex.clear();
+            m_nlsat->get_core(core);
+            for (auto c : core) {
+                unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
+                ex.push_justification(idx, rational(1));
+                TRACE("arith", tout << "ex: " << idx << "\n";);
             }
-            catch (z3_exception&) {
-                if (m_limit.get_cancel_flag()) {
-                    r = l_undef;
-                }
-                else {
-                    throw;
-                }
-            }
-            TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
-            switch (r) {
-            case l_true: 
-                break;
-            case l_false: 
-                ex.clear();
-                m_nlsat->get_core(core);
-                for (auto c : core) {
-                    unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
-                    ex.push_justification(idx, rational(1));
-                    TRACE("arith", tout << "ex: " << idx << "\n";);
-                }
-                break;
+            break;
 
-            case l_undef:
-                break;
-            }            
-            return r;
-        }                
+        case l_undef:
+            break;
+        }            
+        return r;
+    }                
 
-        void add_monic_eq(mon_eq const& m) {
-            polynomial::manager& pm = m_nlsat->pm();
-            svector<polynomial::var> vars;
+    void add_monic_eq(mon_eq const& m) {
+        polynomial::manager& pm = m_nlsat->pm();
+        svector<polynomial::var> vars;
+        for (auto v : m.vars()) {
+            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(m.var()), 1), pm);
+        polynomial::monomial * mls[2] = { m1, m2 };
+        polynomial::scoped_numeral_vector coeffs(pm.m());
+        coeffs.push_back(mpz(1));
+        coeffs.push_back(mpz(-1));
+        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 = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
+        m_nlsat->mk_clause(1, &lit, nullptr);
+    }
+
+    void add_constraint(unsigned idx) {
+        auto& c = s.constraints()[idx];
+        auto& pm = m_nlsat->pm();
+        auto k = c.kind();
+        auto rhs = c.rhs();
+        auto lhs = c.coeffs();
+        auto sz = lhs.size();
+        svector<polynomial::var> vars;
+        rational den = denominator(rhs);
+        for (auto kv : lhs) {
+            vars.push_back(lp2nl(kv.second));
+            den = lcm(den, denominator(kv.first));
+        }
+        vector<rational> coeffs;
+        for (auto kv : lhs) {
+            coeffs.push_back(den * kv.first);
+        }
+        rhs *= den;
+        polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm);
+        polynomial::polynomial* ps[1] = { p };
+        bool is_even[1] = { false };
+        nlsat::literal lit;
+        nlsat::assumption a = this + idx;
+        switch (k) {
+        case lp::lconstraint_kind::LE:
+            lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
+            break;
+        case lp::lconstraint_kind::GE:
+            lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
+            break;
+        case lp::lconstraint_kind::LT:
+            lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
+            break;
+        case lp::lconstraint_kind::GT:
+            lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
+            break;
+        case lp::lconstraint_kind::EQ:
+            lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);                
+            break;
+        default:
+            lp_assert(false); // unreachable
+        }
+        m_nlsat->mk_clause(1, &lit, a);
+    }               
+
+    bool is_int(lp::var_index v) {
+        return s.var_is_int(v);
+    }
+
+
+    polynomial::var lp2nl(lp::var_index v) {
+        polynomial::var r;
+        if (!m_lp2nl.find(v, r)) {
+            r = m_nlsat->mk_var(is_int(v));
+            m_lp2nl.insert(v, r);
+            TRACE("arith", tout << "j" << v << " := x" << r << "\n";);
+        }
+        return r;
+    }
+
+    nlsat::anum const& value(lp::var_index v) const {
+        polynomial::var pv;
+        if (m_lp2nl.find(v, pv))
+            return m_nlsat->value(pv);
+        else
+            return *m_zero;
+    }
+
+    nlsat::anum_manager& am() {
+        return m_nlsat->am();
+    }
+
+    std::ostream& display(std::ostream& out) const {
+        for (auto m : m_monics) {
+            out << "j" << m.var() << " = ";
             for (auto v : m.vars()) {
-                vars.push_back(lp2nl(v));
+                out << "j" << v << " ";
             }
-            polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
-            polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.var()), 1), pm);
-            polynomial::monomial * mls[2] = { m1, m2 };
-            polynomial::scoped_numeral_vector coeffs(pm.m());
-            coeffs.push_back(mpz(1));
-            coeffs.push_back(mpz(-1));
-            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 = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
-            m_nlsat->mk_clause(1, &lit, nullptr);
+            out << "\n";
         }
-
-        void add_constraint(unsigned idx) {
-            auto& c = s.constraints()[idx];
-            auto& pm = m_nlsat->pm();
-            auto k = c.kind();
-            auto rhs = c.rhs();
-            auto lhs = c.coeffs();
-            auto sz = lhs.size();
-            svector<polynomial::var> vars;
-            rational den = denominator(rhs);
-            for (auto kv : lhs) {
-                vars.push_back(lp2nl(kv.second));
-                den = lcm(den, denominator(kv.first));
-            }
-            vector<rational> coeffs;
-            for (auto kv : lhs) {
-                coeffs.push_back(den * kv.first);
-            }
-            rhs *= den;
-            polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm);
-            polynomial::polynomial* ps[1] = { p };
-            bool is_even[1] = { false };
-            nlsat::literal lit;
-            nlsat::assumption a = this + idx;
-            switch (k) {
-            case lp::lconstraint_kind::LE:
-                lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
-                break;
-            case lp::lconstraint_kind::GE:
-                lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
-                break;
-            case lp::lconstraint_kind::LT:
-                lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
-                break;
-            case lp::lconstraint_kind::GT:
-                lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
-                break;
-            case lp::lconstraint_kind::EQ:
-                lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);                
-                break;
-            default:
-                lp_assert(false); // unreachable
-            }
-            m_nlsat->mk_clause(1, &lit, a);
-        }               
-
-        bool is_int(lp::var_index v) {
-            return s.var_is_int(v);
-        }
-
-
-        polynomial::var lp2nl(lp::var_index v) {
-            polynomial::var r;
-            if (!m_lp2nl.find(v, r)) {
-                r = m_nlsat->mk_var(is_int(v));
-                m_lp2nl.insert(v, r);
-                TRACE("arith", tout << "j" << v << " := x" << r << "\n";);
-            }
-            return r;
-        }
-
-        nlsat::anum const& value(lp::var_index v) const {
-            polynomial::var pv;
-            if (m_lp2nl.find(v, pv))
-                return m_nlsat->value(pv);
-            else
-                return *m_zero;
-        }
-
-        nlsat::anum_manager& am() {
-            return m_nlsat->am();
-        }
-
-        std::ostream& display(std::ostream& out) const {
-            for (auto m : m_monics) {
-                out << "j" << m.var() << " = ";
-                for (auto v : m.vars()) {
-                    out << "j" << v << " ";
-                }
-                out << "\n";
-            }
-            return out;
-        }
-    };
-
-    solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
-        m_imp = alloc(imp, s, lim, p);
+        return out;
     }
+};
 
-    solver::~solver() {
-        dealloc(m_imp);
-    }
+solver::solver(lp::lar_solver& s, reslimit& lim, nla::core & nla_core, params_ref const& p) {
+    m_imp = alloc(imp, s, lim, p, nla_core);
+}
 
-    void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) {
-        m_imp->add(v, sz, vs);
-    }
+solver::~solver() {
+    dealloc(m_imp);
+}
 
-    lbool solver::check(lp::explanation& ex) {
-        return m_imp->check(ex);
-    }
+void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) {
+    m_imp->add(v, sz, vs);
+}
 
-    bool solver::need_check() {
-        return m_imp->need_check();
-    }
+lbool solver::check(lp::explanation& ex) {
+    return m_imp->check(ex);
+}
 
-    void solver::push() {
-        m_imp->push();
-    }
+bool solver::need_check() {
+    return m_imp->need_check();
+}
 
-    void solver::pop(unsigned n) {
-        m_imp->pop(n);
-    }
+void solver::push() {
+    m_imp->push();
+}
 
-    std::ostream& solver::display(std::ostream& out) const {
-        return m_imp->display(out);
-    }
+void solver::pop(unsigned n) {
+    m_imp->pop(n);
+}
 
-    nlsat::anum const& solver::value(lp::var_index v) const {
-        return m_imp->value(v);
-    }
+std::ostream& solver::display(std::ostream& out) const {
+    return m_imp->display(out);
+}
 
-    nlsat::anum_manager& solver::am() {
-        return m_imp->am();
-    }
+nlsat::anum const& solver::value(lp::var_index v) const {
+    return m_imp->value(v);
+}
+
+nlsat::anum_manager& solver::am() {
+    return m_imp->am();
+}
 
 }
diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h
index d8af073ef..0303b76be 100644
--- a/src/math/lp/nra_solver.h
+++ b/src/math/lp/nra_solver.h
@@ -25,7 +25,7 @@ namespace nra {
 
     public:
 
-        solver(lp::lar_solver& s, reslimit& lim, params_ref const& p = params_ref());
+        solver(lp::lar_solver& s, reslimit& lim, nla::core & nla_core, params_ref const& p = params_ref());
         
         ~solver();
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index bd0afe80f..ca2afce59 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -24,7 +24,6 @@
 #include "math/lp/lp_dual_simplex.h"
 #include "math/lp/indexed_value.h"
 #include "math/lp/lar_solver.h"
-#include "math/lp/nra_solver.h"
 #include "math/lp/nla_solver.h"
 #include "math/lp/lp_types.h"
 #include "math/polynomial/algebraic_numbers.h"
@@ -268,57 +267,21 @@ class theory_lra::imp {
     unsigned                                          m_num_conflicts;
 
     // non-linear arithmetic
-    scoped_ptr<nra::solver>  m_nra;
     scoped_ptr<nla::solver>  m_nla;
-    bool                     m_use_nra_model;
     scoped_ptr<scoped_anum>  m_a1, m_a2;
 
     struct switcher {
         theory_lra::imp& m_th_imp;
-        scoped_ptr<nra::solver>*  m_nra;
         scoped_ptr<nla::solver>*  m_nla;
-        bool                      m_use_nla;
-        switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_nla(nullptr) {
+        switcher(theory_lra::imp& i): m_th_imp(i), m_nla(nullptr) {
         }
-
+        
         bool need_check() {
-            if (m_use_nla) {
-                if (m_nla != nullptr)
-                    return (*m_nla)->need_check();
-            }
-            else {
-                if (m_nra != nullptr)
-                    return (*m_nra)->need_check();
-            }
+            if (m_nla != nullptr)
+                return (*m_nla)->need_check();
             return false;
         }
-        
-        void push() {
-            if (m_nla != nullptr)
-                (*m_nla)->push();
-            if (m_nra != nullptr)
-                (*m_nra)->push();
-        }
-
-        void pop(unsigned scopes) {
-            if (m_nla != nullptr)
-                (*m_nla)->pop(scopes);
-            if (m_nra != nullptr)
-                (*m_nra)->pop(scopes);
-        }
-
-        
-        void add_monic(lpvar v, unsigned sz, lpvar const* vs) {
-            if (m_use_nla) {
-                m_th_imp.ensure_nla();
-                (*m_nla)->add_monic(v, sz, vs);
-            }
-            else {
-                m_th_imp.ensure_nra();
-                (*m_nra)->add_monic(v, sz, vs);
-            }
-        }
- 
+                
     };
 
     // integer arithmetic
@@ -339,12 +302,7 @@ class theory_lra::imp {
         imp & m_th;
         var_value_hash(imp & th):m_th(th) {}
         unsigned operator()(theory_var v) const { 
-            if (m_th.m_use_nra_model) {
-                return m_th.is_int(v);
-            }
-            else {
-                return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v)); 
-            }
+            return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v));             
         }
     };
     int_hashtable<var_value_hash, var_value_eq>   m_model_eqs;
@@ -373,15 +331,39 @@ class theory_lra::imp {
     lp::lar_solver& lp(){ return *m_solver.get(); }
     const lp::lar_solver& lp() const { return *m_solver.get(); }
     
-    void ensure_nra() {
-        if (!m_nra) {
-            m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params());
-            m_switcher.m_nra = &m_nra;
-            for (auto const& _s : m_scopes) {
-                (void)_s;
-                m_nra->push();
-            }
-        }
+    void init_solver() {
+        if (m_solver) return;
+
+        reset_variable_values();
+        m_solver = alloc(lp::lar_solver); 
+
+        // initialize 0, 1 variables:
+        get_one(true);
+        get_one(false);
+        get_zero(true);
+        get_zero(false);
+
+        smt_params_helper lpar(ctx().get_params());
+        lp().settings().set_resource_limit(m_resource_limit);
+        lp().settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lpar.arith_simplex_strategy());
+        lp().settings().bound_propagation() = BP_NONE != propagation_mode();
+        lp().settings().m_enable_hnf = lpar.arith_enable_hnf();
+        lp().settings().m_print_external_var_name = lpar.arith_print_ext_var_names();
+        lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows());
+        lp().settings().report_frequency = lpar.arith_rep_freq();
+        lp().settings().print_statistics = lpar.arith_print_stats();
+
+        // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
+        unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
+        lp().set_cut_strategy(branch_cut_ratio);
+        
+        lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
+        lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
+        m_lia = alloc(lp::int_solver, *m_solver.get());
+        get_one(true);
+        get_zero(true);
+        get_one(false);
+        get_zero(false);
     }
 
     lpvar add_const(int c, lpvar& var, bool is_int) {
@@ -410,7 +392,6 @@ class theory_lra::imp {
     void ensure_nla() {
         if (!m_nla) {
             m_nla = alloc(nla::solver, *m_solver.get());
-            m_switcher.m_nla = &m_nla;
             for (auto const& _s : m_scopes) {
                 (void)_s;
                 m_nla->push();
@@ -667,7 +648,7 @@ class theory_lra::imp {
             }
             TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
             m_solver->register_existing_terms();            
-            m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
+            m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
         }
         return v;
     }
@@ -973,7 +954,6 @@ public:
         m_asserted_qhead(0), 
         m_assume_eq_head(0),
         m_num_conflicts(0),
-        m_use_nra_model(false),
         m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
         m_solver(nullptr),
         m_resource_limit(*this),
@@ -1187,7 +1167,9 @@ public:
         sc.m_not_handled = m_not_handled;
         sc.m_underspecified_lim = m_underspecified.size();
         lp().push();
-        m_switcher.push();
+        if (m_nla)
+            m_nla->push();
+
     }
 
     void pop_scope_eh(unsigned num_scopes) {
@@ -1207,7 +1189,8 @@ public:
         // VERIFY(l_false != make_feasible());
         m_new_bounds.reset();
         m_to_check.reset();
-        m_switcher.pop(num_scopes);
+        if (m_nla)
+            m_nla->pop(num_scopes);
         TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
     }
 
@@ -1588,7 +1571,7 @@ public:
     }
 
     void random_update() {
-        if (m_use_nra_model || m_nla)
+        if (m_nla)
             return;
         m_tmp_var_set.clear();
         m_tmp_var_set.resize(th.get_num_vars());
@@ -1696,13 +1679,7 @@ public:
     }
 
     bool is_eq(theory_var v1, theory_var v2) {
-        if (m_use_nra_model) {
-            SASSERT(!m_switcher.m_use_nla);
-            return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
-        }
-        else {
-            return get_ivalue(v1) == get_ivalue(v2); 
-        }
+        return get_ivalue(v1) == get_ivalue(v2); 
     }
 
     bool has_delayed_constraints() const {
@@ -1712,7 +1689,6 @@ public:
     final_check_status final_check_eh() {
         reset_variable_values();
         IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
-        m_use_nra_model = false;
         lbool is_sat = l_true;
         SASSERT(lp().ax_is_correct());
         if (lp().get_status() != lp::lp_status::OPTIMAL) {
@@ -2140,27 +2116,6 @@ public:
         return lia_check;
     }
 
-    lbool check_aftermath_nra(lbool r) {
-        m_a1 = alloc(scoped_anum, m_nra->am());
-        m_a2 = alloc(scoped_anum, m_nra->am());
-        switch (r) {
-        case l_false:
-            set_conflict();
-            break;
-        case l_true:
-            m_use_nra_model = true;
-            if (assume_eqs()) {
-                return l_false;
-            }
-            break;
-        case l_undef:
-            TRACE("arith", tout << "nra-undef\n";);
-        default:
-            break;
-        }
-        return r;
-    }
-
     nla::lemma m_lemma;
  
     void false_case_of_check_nla(const nla::lemma & l) {
@@ -2196,7 +2151,10 @@ public:
         set_conflict_or_lemma(core, false);
     }
     
-    lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& lv) {
+    lbool check_nra_continue() {
+        m_a1 = nullptr; m_a2 = nullptr;
+        auto & lv = m_nla_lemma_vector;
+        lbool r = m_nla->check(lv);
         switch (r) {
         case l_false: {
             m_stats.m_nla_lemmas += lv.size();
@@ -2217,20 +2175,13 @@ public:
     }
 
     lbool check_nra() {
-        m_use_nra_model = false;
         if (!m.inc()) {
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
-        if (!m_nra && !m_nla) return l_true;
+        if (!m_nla) return l_true;
         if (!m_switcher.need_check()) return l_true;
-        m_a1 = nullptr; m_a2 = nullptr;
-        if (m_nra) {
-            m_explanation.clear();
-            return check_aftermath_nra(m_nra->check(m_explanation));
-        }
-        vector<nla::lemma> lv;
-        return check_aftermath_nla(m_nla->check(lv), lv);
+        return check_nra_continue();
     }
 
     /**
@@ -3259,7 +3210,7 @@ public:
     }
  
     lp::explanation     m_explanation;
-    
+    vector<nla::lemma>  m_nla_lemma_vector;
     literal_vector      m_core;
     svector<enode_pair> m_eqs;
     vector<parameter>   m_params;
@@ -3363,7 +3314,6 @@ public:
     }
 
     void reset_eh() {
-        m_use_nra_model = false;
         m_arith_eq_adapter.reset_eh();
         m_solver = nullptr;
         m_internalize_head = 0;
@@ -3385,65 +3335,14 @@ public:
         TRACE("arith", display(tout););
     }
 
-    nlsat::anum const& nl_value(theory_var v, scoped_anum& r) {
-        SASSERT(m_nra);
-        SASSERT(m_use_nra_model);
-        auto t = get_tv(v);
-        if (t.is_term()) {
-
-            m_todo_terms.push_back(std::make_pair(t, rational::one()));
-
-            TRACE("arith", tout << "v" << v << " := w" << t.to_string() << "\n";
-                  lp().print_term(lp().get_term(t), tout) << "\n";);
-
-            m_nra->am().set(r, 0);
-            while (!m_todo_terms.empty()) {
-                rational wcoeff = m_todo_terms.back().second;
-                t = m_todo_terms.back().first;
-                m_todo_terms.pop_back();
-                lp::lar_term const& term = lp().get_term(t);
-                TRACE("arith", lp().print_term(term, tout) << "\n";);
-                scoped_anum r1(m_nra->am());
-                rational c1(0);
-                m_nra->am().set(r1, c1.to_mpq());
-                m_nra->am().add(r, r1, r);                
-                for (auto const & arg : term) {
-                    auto wi = lp().column2tv(arg.column());
-                    c1 = arg.coeff() * wcoeff;
-                    if (wi.is_term()) {
-                        m_todo_terms.push_back(std::make_pair(wi, c1));
-                    }
-                    else {
-                        m_nra->am().set(r1, c1.to_mpq());
-                        m_nra->am().mul(m_nra->value(wi.id()), r1, r1);
-                        m_nra->am().add(r1, r, r);
-                    }
-                }
-            }
-            return r;
-        }
-        else {
-            return m_nra->value(t.id());
-        }
-    }
-
     model_value_proc * mk_value(enode * n, model_generator & mg) {
         theory_var v = n->get_th_var(get_id());
         expr* o = n->get_owner();
-        if (m_use_nra_model) {
-            anum const& an = nl_value(v, *m_a1);
-            if (a.is_int(o) && !m_nra->am().is_int(an)) {
-                return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o)));
-            }
-            return alloc(expr_wrapper_proc, a.mk_numeral(nl_value(v, *m_a1), a.is_int(o)));
-        }
-        else {
-            rational r = get_value(v);
-            TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
-            SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
-            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)));
-        }
+        rational r = get_value(v);
+        TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
+        SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
+        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, rational& val) {
@@ -3818,9 +3717,6 @@ public:
         if (m_nla) {
             m_nla->display(out);
         }
-        if (m_nra) {
-            m_nra->display(out);
-        }
         unsigned nv = th.get_num_vars();
         for (unsigned v = 0; v < nv; ++v) {
             auto t = get_tv(v);