diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 31dff1715..c9f9dc270 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -97,7 +97,6 @@ add_subdirectory(tactic/portfolio)
 add_subdirectory(opt)
 add_subdirectory(api)
 add_subdirectory(api/dll)
-add_definitions(-DDUMP_ARGS)
 ################################################################################
 # libz3
 ################################################################################
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 55361e028..856089abe 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1902,7 +1902,7 @@ void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
     ex.display(std::cout, ps);
 }
 void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
-    //    ex.display(std::cout, x);
+    ex.display(std::cout, x);
     std::cout << std::endl;
 }
 void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 9a21435fb..b2d48b1be 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -301,12 +301,6 @@ static void parse_cmd_line_args(int argc, char ** argv) {
 
 
 int STD_CALL main(int argc, char ** argv) {
-#ifdef DUMP_ARGS_
-     std::cout << "args are: ";
-     for (int i = 0; i < argc; i++)
-         std::cout << argv[i] <<" ";
-     std::cout << std::endl;
-#endif
      try{
         unsigned return_value = 0;
         memory::initialize(0);
diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt
index bbdcae080..2741334b4 100644
--- a/src/tactic/smtlogics/CMakeLists.txt
+++ b/src/tactic/smtlogics/CMakeLists.txt
@@ -40,4 +40,3 @@ z3_add_component(smtlogic_tactics
     qfufbv_tactic.h
     quant_tactics.h
 )
-add_definitions(-DSTART_ONLY_QFNIA_SMT)
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 56b3c76b9..687a39f6f 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -118,10 +118,11 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
 
     return and_then(
         mk_report_verbose_tactic("(qfnia-tactic)", 10),
-        mk_qfnia_preamble(m, p),
+        mk_qfnia_premable(m, p),
         or_else(mk_qfnia_sat_solver(m, p),
                 try_for(mk_qfnia_smt_solver(m, p), 2000),
                 mk_qfnia_nlsat_solver(m, p),
-                mk_qfnia_smt_solver(m, p))<
-                    );
+                mk_qfnia_smt_solver(m, p))
+               )
+        ;
 }
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 830a06c2a..fb0e939ca 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -2761,10 +2761,10 @@ void test_bound_propagation_one_small_sample1() {
     vector<std::pair<mpq, var_index>> coeffs;
     coeffs.push_back(std::pair<mpq, var_index>(mpq(1), a));
     coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), c));
-    ls.add_term(coeffs);
+    ls.add_term(coeffs, -1);
     coeffs.pop_back();
     coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), b));
-    ls.add_term(coeffs);
+    ls.add_term(coeffs, -1);
     coeffs.clear();
     coeffs.push_back(std::pair<mpq, var_index>(mpq(1), a));
     coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), b));
@@ -2825,8 +2825,7 @@ void test_bound_propagation_one_row() {
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(mpq(1), x0));
     c.push_back(std::pair<mpq, var_index>(mpq(-1), x1));
-    explanation e;
-    ls.add_constraint(c, EQ, one_of_type<mpq>(), e);
+    ls.add_constraint(c, EQ, one_of_type<mpq>());
     vector<implied_bound> ev;
     ls.add_var_bound(x0, LE, mpq(1));
     ls.solve();
@@ -2840,8 +2839,7 @@ void test_bound_propagation_one_row_with_bounded_vars() {
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(mpq(1), x0));
     c.push_back(std::pair<mpq, var_index>(mpq(-1), x1));
-    explanation e;
-    ls.add_constraint(c, EQ, one_of_type<mpq>(), e);
+    ls.add_constraint(c, EQ, one_of_type<mpq>());
     vector<implied_bound> ev;
     ls.add_var_bound(x0, GE, mpq(-3));
     ls.add_var_bound(x0, LE, mpq(3));
@@ -2857,8 +2855,7 @@ void test_bound_propagation_one_row_mixed() {
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(mpq(1), x0));
     c.push_back(std::pair<mpq, var_index>(mpq(-1), x1));
-    explanation e;
-    ls.add_constraint(c, EQ, one_of_type<mpq>(), e);
+    ls.add_constraint(c, EQ, one_of_type<mpq>());
     vector<implied_bound> ev;
     ls.add_var_bound(x1, LE, mpq(1));
     ls.solve();
diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp
index 38419177c..1553b7363 100644
--- a/src/util/lp/factorization.cpp
+++ b/src/util/lp/factorization.cpp
@@ -28,7 +28,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
         k.type() = factor_type::VAR;
     } else {
         unsigned i;
-        if (!m_ff->find_rm_monomial_of_vars(k_vars,i)) {
+        if (!m_ff->find_rm_monomial_of_vars(k_vars, i)) {
             return false;
         }
         k.index() = i;
@@ -49,7 +49,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
     return true;
 }
 
-const_iterator_mon::reference const_iterator_mon::operator*() const {
+factorization const_iterator_mon::operator*() const {
     if (m_full_factorization_returned == false)  {
         return create_full_factorization();
     }
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index c325e1ee0..05e78442a 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -73,7 +73,6 @@ struct const_iterator_mon {
     //typedefs
     typedef const_iterator_mon self_type;
     typedef factorization value_type;
-    typedef const factorization reference;
     typedef int difference_type;
     typedef std::forward_iterator_tag iterator_category;
 
@@ -81,7 +80,7 @@ struct const_iterator_mon {
             
     bool get_factors(factor& k, factor& j, rational& sign) const;
 
-    reference operator*() const;
+    factorization operator*() const;
     void advance_mask();
             
     self_type operator++();
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index ee40a0916..c90626946 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1618,7 +1618,7 @@ bool lar_solver::strategy_is_undecided() const {
     return m_settings.simplex_strategy() == simplex_strategy_enum::undecided;
 }
 
-var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, std::string name) {
+var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::string& name) {
     var_index j = add_var(ext_j,is_int);
     m_var_register.set_name(j, name);
     return j;
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 59d9e0e6f..b8fe67ba2 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -163,7 +163,7 @@ public:
 
     var_index add_var(unsigned ext_j, bool is_integer);
 
-    var_index add_named_var(unsigned ext_j, bool is_integer, std::string);
+    var_index add_named_var(unsigned ext_j, bool is_integer, const std::string&);
 
     void register_new_ext_var_index(unsigned ext_v, bool is_int);
 
diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/util/lp/lp_core_solver_base_def.h
index 7da84cfc3..23529ffff 100644
--- a/src/util/lp/lp_core_solver_base_def.h
+++ b/src/util/lp/lp_core_solver_base_def.h
@@ -697,7 +697,7 @@ non_basis_is_correctly_represented_in_heading() const {
 
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
     basis_heading_is_correct() const {
-    if ( m_A.column_count() > 10 ) {
+    if ( m_A.column_count() > 10 ) { // for the performance reason
         return true;
     }
     lp_assert(m_basis_heading.size() == m_A.column_count());
diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h
index 548062f68..408878dae 100644
--- a/src/util/lp/monomial.h
+++ b/src/util/lp/monomial.h
@@ -1,6 +1,8 @@
 /*
   Copyright (c) 2017 Microsoft Corporation
   Author: Nikolaj Bjorner
+          Lev Nachmanson
+      
 */
 #pragma once
 #include "util/lp/lp_settings.h"
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index ec0aec2ed..a49112c9a 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -180,7 +180,7 @@ struct solver::imp {
 
     lpvar var(const factor& f) const {
         return f.is_var()?
-            f.index() : var(m_rm_table.vec()[f.index()]);
+            f.index() : var(m_rm_table.rms()[f.index()]);
     }
 
     svector<lpvar> sorted_vars(const factor& f) const {
@@ -189,14 +189,14 @@ struct solver::imp {
             return r;
         }
         TRACE("nla_solver", tout << "nv";);
-        return m_rm_table.vec()[f.index()].vars();
+        return m_rm_table.rms()[f.index()].vars();
     }
 
     // the value of the factor is equal to the value of the variable multiplied
     // by the flip_sign
     rational flip_sign(const factor& f) const {
         return f.is_var()?
-            flip_sign_of_var(f.index()) : m_rm_table.vec()[f.index()].orig_sign();
+            flip_sign_of_var(f.index()) : m_rm_table.rms()[f.index()].orig_sign();
     }
 
     rational flip_sign_of_var(lpvar j) const {
@@ -282,7 +282,7 @@ struct solver::imp {
         if (f.type() == factor_type::VAR) {
             m_vars_equivalence.explain(f.index(), exp);
         } else {
-            m_vars_equivalence.explain(m_monomials[m_rm_table.vec()[f.index()].orig_index()], exp);
+            m_vars_equivalence.explain(m_monomials[m_rm_table.rms()[f.index()].orig_index()], exp);
         }
     }
 
@@ -305,7 +305,7 @@ struct solver::imp {
             print_var(f.index(), out);
         } else {
             out << "PROD, ";
-            print_product(m_rm_table.vec()[f.index()].vars(), out);
+            print_product(m_rm_table.rms()[f.index()].vars(), out);
         }
         out << "\n";
         return out;
@@ -315,8 +315,8 @@ struct solver::imp {
         if (f.is_var()) {
             print_var(f.index(), out);
         } else {
-            out << " RM = "; print_rooted_monomial_with_vars(m_rm_table.vec()[f.index()], out);
-            out << "\n orig mon = "; print_monomial_with_vars(m_monomials[m_rm_table.vec()[f.index()].orig_index()], out);
+            out << " RM = "; print_rooted_monomial_with_vars(m_rm_table.rms()[f.index()], out);
+            out << "\n orig mon = "; print_monomial_with_vars(m_monomials[m_rm_table.rms()[f.index()].orig_index()], out);
         }
         return out;
     }
@@ -929,7 +929,7 @@ struct solver::imp {
         if (!try_insert(k, explored))
             return false;
 
-        const auto& mons_to_explore = m_rm_table.vec()[k].m_mons;
+        const auto& mons_to_explore = m_rm_table.rms()[k].m_mons;
         
         for (index_with_sign i_s : mons_to_explore) {
             unsigned n = i_s.index();
@@ -1027,7 +1027,7 @@ struct solver::imp {
                 print_var(f[k].index(), out);
             else {
                 out << "(";
-                print_product(m_rm_table.vec()[f[k].index()].vars(), out);
+                print_product(m_rm_table.rms()[f[k].index()].vars(), out);
                 out << ")";
             }
             
@@ -1039,15 +1039,15 @@ struct solver::imp {
     
     bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
         SASSERT(vars_are_roots(vars));
-        auto it = m_rm_table.map().find(vars);
-        if (it == m_rm_table.map().end()) {
+        auto it = m_rm_table.vars_key_to_rm_index().find(vars);
+        if (it == m_rm_table.vars_key_to_rm_index().end()) {
             return false;
         }
         
         i = it->second;
         TRACE("nla_solver",);
         
-        SASSERT(lp::vectors_are_equal_(vars, m_rm_table.vec()[i].vars()));
+        SASSERT(lp::vectors_are_equal_(vars, m_rm_table.rms()[i].vars()));
         return true;
     }
 
@@ -1648,7 +1648,7 @@ struct solver::imp {
         unsigned start = random() % rm_ref.size();
         unsigned i = start;
         do {
-            const rooted_mon& r = m_rm_table.vec()[rm_ref[i]];
+            const rooted_mon& r = m_rm_table.rms()[rm_ref[i]];
             SASSERT (!check_monomial(m_monomials[r.orig_index()]));
             basic_lemma_for_mon(r, derived);
             if (++i == rm_ref.size()) {
@@ -1756,7 +1756,7 @@ struct solver::imp {
     }
 
     bool rm_table_is_ok() const {
-        for (const auto & rm : m_rm_table.vec()) {
+        for (const auto & rm : m_rm_table.rms()) {
             for (lpvar j : rm.vars()) {
                 if (!m_vars_equivalence.is_root(j)){
                     TRACE("nla_solver", print_var(j, tout););
@@ -1800,7 +1800,7 @@ struct solver::imp {
         for (auto j : p) {
             out << "\nj = " << j <<
                 ", rm = ";
-            print_rooted_monomial(m_rm_table.vec()[j], out);
+            print_rooted_monomial(m_rm_table.rms()[j], out);
         }
         out << "\n}";
     }
@@ -1812,8 +1812,8 @@ struct solver::imp {
             if (abs(vvr(mc.vars()[i])) == rational(1)) {
                 auto vv = mc.vars();
                 vv.erase(vv.begin()+i);
-                auto it = m_rm_table.map().find(vv);
-                if (it == m_rm_table.map().end()) {
+                auto it = m_rm_table.vars_key_to_rm_index().find(vv);
+                if (it == m_rm_table.vars_key_to_rm_index().end()) {
                     out << "nf length" << vv.size() << "\n"; ;
                 }
             }
@@ -1881,8 +1881,8 @@ struct solver::imp {
             b = factor(b_vars[0]);
             return true;
         }
-        auto it = m_rm_table.map().find(b_vars);
-        if (it == m_rm_table.map().end()) {
+        auto it = m_rm_table.vars_key_to_rm_index().find(b_vars);
+        if (it == m_rm_table.vars_key_to_rm_index().end()) {
             TRACE("nla_solver_div", tout << "not in rooted";);
             return false;
         }
@@ -2088,7 +2088,7 @@ struct solver::imp {
             SASSERT(m_monomials[it->second].var() == i && abs(vvr(m_monomials[it->second])) == abs(vvr(c)));
             const index_with_sign & i_s = m_rm_table.get_rooted_mon(it->second);
             unsigned rm_i = i_s.index();
-            //                SASSERT(abs(vvr(m_rm_table.vec()[i])) == abs(vvr(c)));
+            //                SASSERT(abs(vvr(m_rm_table.rms()[i])) == abs(vvr(c)));
             if (try_insert(rm_i, found_rm)) {
                 r.push_back(factor(rm_i, factor_type::RM));
                 TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(rm_i, factor_type::RM), tout); );
@@ -2114,13 +2114,13 @@ struct solver::imp {
             TRACE("nla_solver", tout << "var(d) = " << var(d););
             for (unsigned rm_bd : m_rm_table.var_map()[d.index()]) {
                 TRACE("nla_solver", );
-                if (order_lemma_on_ac_and_bd(rm ,ac, k, m_rm_table.vec()[rm_bd], d)) {
+                if (order_lemma_on_ac_and_bd(rm ,ac, k, m_rm_table.rms()[rm_bd], d)) {
                     return true;
                 }
             }
         } else {
             for (unsigned rm_b : m_rm_table.proper_factors()[d.index()]) {
-                if (order_lemma_on_ac_and_bd(rm , ac, k, m_rm_table.vec()[rm_b], d)) {
+                if (order_lemma_on_ac_and_bd(rm , ac, k, m_rm_table.rms()[rm_b], d)) {
                     return true;
                 }
             }
@@ -2266,7 +2266,7 @@ struct solver::imp {
         unsigned start = random() % rm_ref.size();
         unsigned i = start;
         do {
-            const rooted_mon& rm = m_rm_table.vec()[rm_ref[i]];
+            const rooted_mon& rm = m_rm_table.rms()[rm_ref[i]];
             order_lemma_on_monomial(rm);
             if (++i == rm_ref.size()) {
                 i = 0;
@@ -2297,8 +2297,8 @@ struct solver::imp {
     // Returns rooted monomials by arity
     std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity() {
         std::unordered_map<unsigned, unsigned_vector> m;
-        for (unsigned i = 0; i < m_rm_table.vec().size(); i++ ) {
-            unsigned arity = m_rm_table.vec()[i].vars().size();
+        for (unsigned i = 0; i < m_rm_table.rms().size(); i++ ) {
+            unsigned arity = m_rm_table.rms()[i].vars().size();
             auto it = m.find(arity);
             if (it == m.end()) {
                 it = m.insert(it, std::make_pair(arity, unsigned_vector()));
@@ -2438,7 +2438,7 @@ struct solver::imp {
               print_rooted_monomial_with_vars(rm, tout); tout << "i = " << i << std::endl;);
         for (unsigned k = i + 1; k < lex_sorted.size(); k++) {
             const auto& p = lex_sorted[k];
-            const rooted_mon& rmk = m_rm_table.vec()[p.second];
+            const rooted_mon& rmk = m_rm_table.rms()[p.second];
             const rational vk = abs(vvr(rmk));
             TRACE("nla_solver", tout << "rmk = ";
                   print_rooted_monomial_with_vars(rmk, tout);
@@ -2470,7 +2470,7 @@ struct solver::imp {
         
         for (unsigned k = i; k-- > 0;) {
             const auto& p = lex_sorted[k];
-            const rooted_mon& rmk = m_rm_table.vec()[p.second];
+            const rooted_mon& rmk = m_rm_table.rms()[p.second];
             const rational vk = abs(vvr(rmk));
             TRACE("nla_solver", tout << "rmk = ";
                   print_rooted_monomial_with_vars(rmk, tout);
@@ -2508,7 +2508,7 @@ struct solver::imp {
     bool monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted) {
         for (unsigned i = 0; i < lex_sorted.size(); i++) {
             unsigned rmi = lex_sorted[i].second;
-            const rooted_mon& rm = m_rm_table.vec()[rmi];
+            const rooted_mon& rm = m_rm_table.rms()[rmi];
             TRACE("nla_solver", print_rooted_monomial(rm, tout); tout << "\n, rm_check = " << rm_check(rm); tout << std::endl;); 
             if ((!rm_check(rm)) && monotonicity_lemma_on_lex_sorted_rm(lex_sorted, i, rm))
                 return true;
@@ -2519,7 +2519,7 @@ struct solver::imp {
     bool monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms) { 
         vector<std::pair<std::vector<rational>, unsigned>> lex_sorted;
         for (unsigned i : rms) {
-            lex_sorted.push_back(std::make_pair(get_sorted_key(m_rm_table.vec()[i]), i));
+            lex_sorted.push_back(std::make_pair(get_sorted_key(m_rm_table.rms()[i]), i));
         }
         std::sort(lex_sorted.begin(), lex_sorted.end(),
                   [](const std::pair<std::vector<rational>, unsigned> &a,
@@ -2535,7 +2535,7 @@ struct solver::imp {
         unsigned ii = i;
         do {
             unsigned rm_i = m_rm_table.m_to_refine[i];
-            monotonicity_lemma(m_rm_table.vec()[rm_i].orig_index());
+            monotonicity_lemma(m_rm_table.rms()[rm_i].orig_index());
             TRACE("nla_solver", print_lemma(tout); );
             if (done()) return;
             i++;
@@ -2606,7 +2606,7 @@ struct solver::imp {
     
     bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const rooted_mon*& rm_found){
         for (unsigned i: m_rm_table.to_refine()) {
-            const auto& rm = m_rm_table.vec()[i]; 
+            const auto& rm = m_rm_table.rms()[i]; 
             SASSERT (!check_monomial(m_monomials[rm.orig_index()]));
             rm_found = &rm;
             if (find_bfc_on_monomial(rm, bf)) {
diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index c7b638410..bd9901392 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -35,16 +35,9 @@ struct ineq {
     bool operator==(const ineq& a) const {
         return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
     }
-    const lp::lar_term& term() const {
-        return m_term;
-    };
-    const lp::lconstraint_kind& cmp() const {
-        return m_cmp;
-    };
-    const rational& rs() const {
-        return m_rs;
-    };
-
+    const lp::lar_term& term() const { return m_term; };
+    lp::lconstraint_kind cmp() const { return m_cmp;  };
+    const rational& rs() const { return m_rs; };
 };
 
 class lemma {
diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h
index 5d8a0e959..207dbfc5d 100644
--- a/src/util/lp/rooted_mons.h
+++ b/src/util/lp/rooted_mons.h
@@ -57,19 +57,19 @@ struct rooted_mon {
 
 struct rooted_mon_table {
     std::unordered_map<svector<lpvar>,
-                       unsigned, // points to vec()
-                       hash_svector>                                 m_map;
-    vector<rooted_mon>                                               m_vector;
-    // for every k 
-    // for each i in m_rooted_monomials_containing_var[k]
-    // m_vector_of_rooted_monomials[i] contains k
+                       unsigned, // points to rms()
+                       hash_svector>                                 m_vars_key_to_rm_index;
+    vector<rooted_mon>                                               m_rms;
+    // for every lpvar k m_mons_containing_var[k]
+    // is the set of all rooted monomials containing
+    // (rather the indices of those pointing to m_rms) 
     std::unordered_map<lpvar, std::unordered_set<unsigned>>          m_mons_containing_var;
 
-    // A map from m_vector_of_rooted_monomials to a set
-    // of sets of m_vector_of_rooted_monomials,
-    // such that for every i and every h in m_proper_factors[i] we have m_vector[i] as a proper factor of m_vector[h]
+    // A map from m_rms_of_rooted_monomials to a set
+    // of sets of m_rms_of_rooted_monomials,
+    // such that for every i and every h in m_proper_factors[i] we have m_rms[i] as a proper factor of m_rms[h]
     std::unordered_map<unsigned, std::unordered_set<unsigned>>       m_proper_factors;
-    // points to m_vector
+    // points to m_rms
     svector<unsigned>                                                m_to_refine;
     // maps the indices of the regular monomials to the rooted monomial indices
     std::unordered_map<unsigned, index_with_sign>                    m_reg_to_rm;
@@ -77,19 +77,21 @@ struct rooted_mon_table {
     void print_stats(std::ostream& out) const {
         static double ratio = 1;
         double s = 0;
-        for (const auto& p : m_map) {
-            s += m_vector[p.second].m_mons.size();
+        for (const auto& p : m_vars_key_to_rm_index) {
+            s += m_rms[p.second].m_mons.size();
         }
-        double r = s /m_map.size();
+        double r = s /m_vars_key_to_rm_index.size();
         if (r > ratio) {
             ratio = r;
-            out << "rooted mons "  << m_map.size() << ", ratio = " << r << "\n";
+            out << "rooted mons "  << m_vars_key_to_rm_index.size() << ", ratio = " << r << "\n";
         }
     }
 
     const svector<unsigned>& to_refine() { return m_to_refine; }
 
     bool list_is_consistent(const vector<index_with_sign>& list, const std::unordered_set<unsigned>& to_refine_reg) const {
+        if (list.begin() == list.end())
+            return false;
         bool t = to_refine_reg.find(list.begin()->index()) == to_refine_reg.end();
         for (const auto& i_s : list) {
             bool tt = to_refine_reg.find(i_s.index()) == to_refine_reg.end();
@@ -108,31 +110,31 @@ struct rooted_mon_table {
     
     void init_to_refine(const std::unordered_set<unsigned>& to_refine_reg) {
         SASSERT(m_to_refine.empty());
-        for (unsigned i = 0; i < vec().size(); i++) {
-            if (list_contains_to_refine_reg(vec()[i].m_mons, to_refine_reg))
+        for (unsigned i = 0; i < rms().size(); i++) {
+            if (list_contains_to_refine_reg(rms()[i].m_mons, to_refine_reg))
                 m_to_refine.push_back(i);
         }
         TRACE("nla_solver", tout << "rooted m_to_refine =["; print_vector(m_to_refine, tout) << "]\n";);
     }
     
     void clear() {
-        m_map.clear();
-        m_vector.clear();
+        m_vars_key_to_rm_index.clear();
+        m_rms.clear();
         m_mons_containing_var.clear();
         m_proper_factors.clear();
         m_to_refine.clear();
         m_reg_to_rm.clear();
     }
     
-    const vector<rooted_mon>& vec() const { return m_vector; }
-    vector<rooted_mon>& vec() { return m_vector; }
+    const vector<rooted_mon>& rms() const { return m_rms; }
+    vector<rooted_mon>& rms() { return m_rms; }
 
-    const std::unordered_map<svector<lpvar>, unsigned, hash_svector> & map() const {
-        return m_map;
+    const std::unordered_map<svector<lpvar>, unsigned, hash_svector> & vars_key_to_rm_index() const {
+        return m_vars_key_to_rm_index;
     }
 
-    std::unordered_map<svector<lpvar>, unsigned, hash_svector> & map() {
-        return m_map;
+    std::unordered_map<svector<lpvar>, unsigned, hash_svector> & vars_key_to_rm_index() {
+        return m_vars_key_to_rm_index;
     }
 
     const std::unordered_map<lpvar, std::unordered_set<unsigned>>& var_map() const {
@@ -151,24 +153,10 @@ struct rooted_mon_table {
         return m_proper_factors;
     }
 
-    void reduce_set_by_checking_proper_containment(std::unordered_set<unsigned>& p,
-                                                   const rooted_mon & rm ) {
-        for (auto it = p.begin(); it != p.end();) {
-            if (lp::is_proper_factor(rm.m_vars, vec()[*it].m_vars)) {
-                it++;
-                continue;
-            }
-            auto iit = it;
-            iit ++;
-            p.erase(it);
-            it = iit;
-        }
-    }
-
-    // here i is the index of a monomial in m_vector
+    // here i is the index of a rooted monomial in m_rms
     void find_rooted_monomials_containing_rm(unsigned i_rm) {
-        const auto & rm = vec()[i_rm];
-    
+        const auto & rm = rms()[i_rm];
+        SASSERT(rm.size() > 1);
         std::unordered_set<unsigned> p = var_map()[rm[0]];
         // TRACE("nla_solver",
         //       tout << "i_rm = " << i_rm << ", rm = ";
@@ -184,19 +172,17 @@ struct rooted_mon_table {
             intersect_set(p, var_map()[rm[k]]);
         }
         // TRACE("nla_solver", trace_print_rms(p, tout););
-        reduce_set_by_checking_proper_containment(p, rm);
-        // TRACE("nla_solver", trace_print_rms(p, tout););
         proper_factors()[i_rm] = p;
     }
 
     void fill_proper_factors() {
-        for (unsigned i = 0; i < vec().size(); i++) {
+        for (unsigned i = 0; i < rms().size(); i++) {
             find_rooted_monomials_containing_rm(i);
         }
     }
 
     void register_rooted_monomial_containing_vars(unsigned i_rm) {
-        for (lpvar j_var : vec()[i_rm].vars()) {
+        for (lpvar j_var : rms()[i_rm].vars()) {
             auto it = var_map().find(j_var);
             if (it == var_map().end()) {
                 std::unordered_set<unsigned> s;
@@ -209,7 +195,7 @@ struct rooted_mon_table {
     }
     
     void fill_rooted_monomials_containing_var() {
-        for (unsigned i = 0; i < vec().size(); i++) {
+        for (unsigned i = 0; i < rms().size(); i++) {
             register_rooted_monomial_containing_vars(i);
         }
     }
@@ -217,15 +203,15 @@ struct rooted_mon_table {
     void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i_mon) {
         index_with_sign ms(i_mon, mc.coeff());
         SASSERT(abs(mc.coeff()) == rational(1));
-        auto it = map().find(mc.vars());
-        if (it == map().end()) {
-            TRACE("nla_solver_rm", tout << "size = " << vec().size(););
-            map().emplace(mc.vars(), vec().size());
-            m_reg_to_rm.emplace(i_mon, index_with_sign(vec().size(), mc.coeff()));
-            vec().push_back(rooted_mon(mc.vars(), i_mon, mc.coeff()));
+        auto it = vars_key_to_rm_index().find(mc.vars());
+        if (it == vars_key_to_rm_index().end()) {
+            TRACE("nla_solver_rm", tout << "size = " << rms().size(););
+            vars_key_to_rm_index().emplace(mc.vars(), rms().size());
+            m_reg_to_rm.emplace(i_mon, index_with_sign(rms().size(), mc.coeff()));
+            rms().push_back(rooted_mon(mc.vars(), i_mon, mc.coeff()));
         } 
         else {
-            vec()[it->second].push_back(ms);
+            rms()[it->second].push_back(ms);
             TRACE("nla_solver_rm", tout << "add ms.m_i = " << ms.m_i;);
             m_reg_to_rm.emplace(i_mon, index_with_sign(it->second, mc.coeff()));
         }
@@ -234,6 +220,5 @@ struct rooted_mon_table {
     const index_with_sign& get_rooted_mon(unsigned i_mon) const {
         return m_reg_to_rm.find(i_mon)->second;
     }
-    
 };
 }
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index f51004a04..bbb19860d 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -87,10 +87,7 @@ struct vars_equivalence {
     // j itself is also included
     svector<lpvar> eq_vars(lpvar j) const {
         svector<lpvar> r = path_to_root(j);
-        svector<lpvar> ch = children(j);
-        for (lpvar k : ch) {
-            r.push_back(k);
-        }
+        r.append(children(j));
         r.push_back(j);
         return r;
     }