diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h
index fe4db08d3..ea16091fe 100644
--- a/src/util/lp/emonomials.h
+++ b/src/util/lp/emonomials.h
@@ -47,9 +47,9 @@ public:
     unsigned& prev() { return m_prev; }
     unsigned visited() const { return m_visited; }
     unsigned& visited() { return m_visited; }
-    svector<lpvar> const& vars() const { return m_rvars; }
-    svector<lp::var_index>::const_iterator begin() const { return vars().begin(); }
-    svector<lp::var_index>::const_iterator end() const { return vars().end(); }
+    svector<lpvar> const& rvars() const { return m_rvars; }
+    svector<lp::var_index>::const_iterator begin() const { return rvars().begin(); }
+    svector<lp::var_index>::const_iterator end() const { return rvars().end(); }
     unsigned size() const { return m_rvars.size(); }
     lpvar operator[](unsigned i) const { return m_rvars[i]; }
     bool sign() const { return m_rsign; }
@@ -97,7 +97,7 @@ class emonomials : public var_eqs_merge_handler {
         hash_canonical(emonomials& em): em(em) {}
             
         unsigned operator()(lpvar v) const {
-            auto const& vec = em.m_canonized[em.m_var2index[v]].vars();
+            auto const& vec = em.m_canonized[em.m_var2index[v]].rvars();
             return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
         }
     };
@@ -112,8 +112,8 @@ class emonomials : public var_eqs_merge_handler {
         emonomials& em;
         eq_canonical(emonomials& em): em(em) {}
         bool operator()(lpvar u, lpvar v) const {
-            auto const& uvec = em.m_canonized[em.m_var2index[u]].vars();
-            auto const& vvec = em.m_canonized[em.m_var2index[v]].vars();
+            auto const& uvec = em.m_canonized[em.m_var2index[u]].rvars();
+            auto const& vvec = em.m_canonized[em.m_var2index[v]].rvars();
             return uvec == vvec;
         }
     };
diff --git a/src/util/lp/factorization_factory_imp.cpp b/src/util/lp/factorization_factory_imp.cpp
index 9d9baac18..a1ef6edc7 100644
--- a/src/util/lp/factorization_factory_imp.cpp
+++ b/src/util/lp/factorization_factory_imp.cpp
@@ -22,7 +22,7 @@
 namespace nla {
         
 factorization_factory_imp::factorization_factory_imp(const smon& rm, const core& s) :
-    factorization_factory(rm.vars(), &s.m_emons[rm.var()]),
+    factorization_factory(rm.rvars(), &s.m_emons[rm.var()]),
     m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }
         
 bool factorization_factory_imp::find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index bb07d60dc..30b84cbf1 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -83,7 +83,7 @@ svector<lpvar> core::sorted_vars(const factor& f) const {
         return r;
     }
     TRACE("nla_solver", tout << "nv";);
-    return m_emons.canonical[f.var()].vars();
+    return m_emons.canonical[f.var()].rvars();
 }
 
 // the value of the factor is equal to the value of the variable multiplied
@@ -170,7 +170,7 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
         print_var(f.var(), out);
     } else {
         out << "PROD, ";
-        print_product(m_emons.canonical[f.var()].vars(), out);
+        print_product(m_emons.canonical[f.var()].rvars(), out);
     }
     out << "\n";
     return out;
@@ -820,7 +820,7 @@ int core::get_derived_sign(const smon& rm, const factorization& f) const {
 }
 void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const {
     out << "rooted vars: ";
-    print_product(rm.vars(), out);
+    print_product(rm.rvars(), out);
     out << "\n";
         
     out << "mon:  " << pp_mon(*this, rm.var()) << "\n";
@@ -1468,11 +1468,11 @@ bool core::divide(const smon& bc, const factor& c, factor & b) const {
           tout << "c_vars = ";
           print_product(c_vars, tout);
           tout << "\nbc_vars = ";
-          print_product(bc.vars(), tout););
-    if (!lp::is_proper_factor(c_vars, bc.vars()))
+          print_product(bc.rvars(), tout););
+    if (!lp::is_proper_factor(c_vars, bc.rvars()))
         return false;
             
-    auto b_vars = lp::vector_div(bc.vars(), c_vars);
+    auto b_vars = lp::vector_div(bc.rvars(), c_vars);
     TRACE("nla_solver_div", tout << "b_vars = "; print_product(b_vars, tout););
     SASSERT(b_vars.size() > 0);
     if (b_vars.size() == 1) {
diff --git a/src/util/lp/nla_monotone_lemmas.cpp b/src/util/lp/nla_monotone_lemmas.cpp
index a39eb4215..28785b4c9 100644
--- a/src/util/lp/nla_monotone_lemmas.cpp
+++ b/src/util/lp/nla_monotone_lemmas.cpp
@@ -120,7 +120,7 @@ bool monotone::monotonicity_lemma_on_lex_sorted(const monotone_array_t& lex_sort
 
 vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const smon& a) const {
     vector<std::pair<rational, lpvar>> r;
-    for (lpvar j : a.vars()) {
+    for (lpvar j : a.rvars()) {
         r.push_back(std::make_pair(abs(vvr(j)), j));
     }
     std::sort(r.begin(), r.end(), [](const std::pair<rational, lpvar>& a,
@@ -220,7 +220,7 @@ void monotone::generate_monl(const smon& a,
 
 std::vector<rational> monotone::get_sorted_key(const smon& rm) const {
     std::vector<rational> r;
-    for (unsigned j : rm.vars()) {
+    for (unsigned j : rm.rvars()) {
         r.push_back(abs(vvr(j)));
     }
     std::sort(r.begin(), r.end());