diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index 4346c8b1c..f6e6d9b66 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -28,7 +28,7 @@ basics::basics(core * c) : common(c) {}
 // Generate a lemma if values of m.var() and n.var() are not the same up to sign
 bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n) {
     const rational& sign = m.rsign() * n.rsign();
-     if (vvr(m) == vvr(n) * sign)
+     if (val(m) == val(n) * sign)
         return false;
     TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";);
     generate_sign_lemma(m, n, sign);
@@ -36,8 +36,8 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial
 }
 
 void basics::generate_zero_lemmas(const monomial& m) {
-    SASSERT(!vvr(m).is_zero() && c().product_value(m.vars()).is_zero());
-    int sign = nla::rat_sign(vvr(m));
+    SASSERT(!val(m).is_zero() && c().product_value(m.vars()).is_zero());
+    int sign = nla::rat_sign(val(m));
     unsigned_vector fixed_zeros;
     lpvar zero_j = find_best_zero(m, fixed_zeros);
     SASSERT(is_set(zero_j));
@@ -77,7 +77,7 @@ bool basics::try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
 }
 
 void basics::get_non_strict_sign(lpvar j, int& sign) const {
-    const rational v = vvr(j);
+    const rational v = val(j);
     if (v.is_zero()) {
         try_get_non_strict_sign_from_bounds(j, sign);
     } else {
@@ -105,7 +105,7 @@ bool basics::basic_sign_lemma_model_based() {
     unsigned sz = c().m_to_refine.size();
     for (unsigned i = sz; i-- > 0; ) {
         monomial const& m = c().m_emons[c().m_to_refine[(start + i) % sz]];
-        int mon_sign = nla::rat_sign(vvr(m));
+        int mon_sign = nla::rat_sign(val(m));
         int product_sign = c().rat_sign(m);
         if (mon_sign != product_sign) {
             basic_sign_lemma_model_based_one_mon(m, product_sign);
@@ -162,12 +162,12 @@ void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rat
     explain(n);        
     TRACE("nla_solver", c().print_lemma(tout););
 }
-// try to find a variable j such that vvr(j) = 0
+// try to find a variable j such that val(j) = 0
 // and the bounds on j contain 0 as an inner point
 lpvar basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
     lpvar zero_j = -1;
     for (unsigned j : m.vars()){
-        if (vvr(j).is_zero()){
+        if (val(j).is_zero()){
             if (c().var_is_fixed_to_zero(j))
                 fixed_zeros.push_back(j);
                 
@@ -204,10 +204,10 @@ void basics::add_fixed_zero_lemma(const monomial& m, lpvar j) {
 }
 void basics::negate_strict_sign(lpvar j) {
     TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";);
-    if (!vvr(j).is_zero()) {
-        int sign = nla::rat_sign(vvr(j));
+    if (!val(j).is_zero()) {
+        int sign = nla::rat_sign(val(j));
         c().mk_ineq(j, (sign == 1? llc::LE : llc::GE));
-    } else {   // vvr(j).is_zero()
+    } else {   // val(j).is_zero()
         if (c().has_lower_bound(j) && c().get_lower_bound(j) >= rational(0)) {
             c().explain_existing_lower_bound(j);
             c().mk_ineq(j, llc::GT);
@@ -322,7 +322,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
     lpvar mon_var =  c().m_emons[rm.var()].var();
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
         
-    const auto mv = vvr(mon_var);
+    const auto mv = val(mon_var);
     const auto abs_mv = abs(mv);
         
     if (abs_mv == rational::zero()) {
@@ -332,7 +332,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
     lpvar jl = -1;
     for (auto fc : f ) {
         lpvar j = var(fc);
-        if (abs(vvr(j)) == abs_mv &&  c().vars_are_equiv(j, mon_var) &&
+        if (abs(val(j)) == abs_mv &&  c().vars_are_equiv(j, mon_var) &&
             (mon_var_is_sep_from_zero ||  c().var_is_separated_from_zero(j))) {
             jl = j;
             break;
@@ -346,7 +346,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
         if (var(j) == jl) {
             continue;
         }
-        if (abs(vvr(j)) != rational(1)) {
+        if (abs(val(j)) != rational(1)) {
             not_one_j = var(j);
             break;
         }
@@ -382,14 +382,14 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monomial& rm, const facto
 
 // x != 0 or y = 0 => |xy| >= |y|
 void basics::proportion_lemma_model_based(const monomial& rm, const factorization& factorization) {
-    rational rmv = abs(vvr(rm));
+    rational rmv = abs(val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
         return;
     }
     int factor_index = 0;
     for (factor f : factorization) {
-        if (abs(vvr(f)) > rmv) {
+        if (abs(val(f)) > rmv) {
             generate_pl(rm, factorization, factor_index);
             return;
         }
@@ -399,14 +399,14 @@ void basics::proportion_lemma_model_based(const monomial& rm, const factorizatio
 // x != 0 or y = 0 => |xy| >= |y|
 bool basics::proportion_lemma_derived(const monomial& rm, const factorization& factorization) {
     return false;
-    rational rmv = abs(vvr(rm));
+    rational rmv = abs(val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
         return false;
     }
     int factor_index = 0;
     for (factor f : factorization) {
-        if (abs(vvr(f)) > rmv) {
+        if (abs(val(f)) > rmv) {
             generate_pl(rm, factorization, factor_index);
             return true;
         }
@@ -418,7 +418,7 @@ bool basics::proportion_lemma_derived(const monomial& rm, const factorization& f
 void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
     add_empty_lemma();
     unsigned mon_var = m.var();
-    rational mv = vvr(mon_var);
+    rational mv = val(mon_var);
     rational sm = rational(nla::rat_sign(mv));
     c().mk_ineq(sm, mon_var, llc::LT);
     for (unsigned fi = 0; fi < m.size(); fi ++) {
@@ -426,7 +426,7 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
         if (fi != factor_index) {
             c().mk_ineq(j, llc::EQ);
         } else {
-            rational jv = vvr(j);
+            rational jv = val(j);
             rational sj = rational(nla::rat_sign(jv));
             SASSERT(sm*mv < sj*jv);
             c().mk_ineq(sj, j, llc::LT);
@@ -449,7 +449,7 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
     }
     add_empty_lemma();
     int fi = 0;
-    rational rmv = vvr(rm);
+    rational rmv = val(rm);
     rational sm = rational(nla::rat_sign(rmv));
     unsigned mon_var = var(rm);
     c().mk_ineq(sm, mon_var, llc::LT);
@@ -458,7 +458,7 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
             c().mk_ineq(var(f), llc::EQ);
         } else {
             lpvar j = var(f);
-            rational jv = vvr(j);
+            rational jv = val(j);
             rational sj = rational(nla::rat_sign(jv));
             SASSERT(sm*rmv < sj*jv);
             c().mk_ineq(sj, j, llc::LT);
@@ -474,7 +474,7 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
 // here we use the fact xy = 0 -> x = 0 or y = 0
 void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const factorization& f) {        
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
-    SASSERT(vvr(rm).is_zero()&& ! c().rm_check(rm));
+    SASSERT(val(rm).is_zero()&& ! c().rm_check(rm));
     add_empty_lemma();
     int sign =  c().get_derived_sign(rm, f);
     if (sign == 0) {
@@ -495,7 +495,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
 
 void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
     TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
-    if (vvr(rm).is_zero()) {
+    if (val(rm).is_zero()) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
                 continue;
@@ -519,14 +519,14 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
     TRACE("nla_solver_bl", c().print_monomial(m, tout););
 
     lpvar mon_var = m.var();
-    const auto mv = vvr(mon_var);
+    const auto mv = val(mon_var);
     const auto abs_mv = abs(mv);
     if (abs_mv == rational::zero()) {
         return false;
     }
     lpvar jl = -1;
     for (auto j : m.vars() ) {
-        if (abs(vvr(j)) == abs_mv) {
+        if (abs(val(j)) == abs_mv) {
             jl = j;
             break;
         }
@@ -538,7 +538,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
         if (j == jl) {
             continue;
         }
-        if (abs(vvr(j)) != rational(1)) {
+        if (abs(val(j)) != rational(1)) {
             not_one_j = j;
             break;
         }
@@ -553,7 +553,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
     c().mk_ineq(mon_var, llc::EQ);
         
     // negate abs(jl) == abs()
-    if (vvr(jl) == - vvr(mon_var))
+    if (val(jl) == - val(mon_var))
         c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma());   
     else  // jl == mon_var
         c().mk_ineq(jl, -rational(1), mon_var, llc::NE);   
@@ -573,7 +573,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
     rational sign(1);
     TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout););
     for (auto j : m.vars()){
-        auto v = vvr(j);
+        auto v = val(j);
         if (v == rational(1)) {
             continue;
         }
@@ -590,7 +590,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
     }
 
     if (not_one + 1) {  // we found the only not_one
-        if (vvr(m) == vvr(not_one) * sign) {
+        if (val(m) == val(not_one) * sign) {
             TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
             return false;
         }
@@ -599,7 +599,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
     add_empty_lemma();
     for (auto j : m.vars()){
         if (not_one == j) continue;
-        c().mk_ineq(j, llc::NE, vvr(j));   
+        c().mk_ineq(j, llc::NE, val(j));   
     }
 
     if (not_one == static_cast<lpvar>(-1)) {
@@ -619,7 +619,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
     lpvar mon_var = c().m_emons[rm.var()].var();
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
         
-    const auto mv = vvr(mon_var);
+    const auto mv = val(mon_var);
     const auto abs_mv = abs(mv);
         
     if (abs_mv == rational::zero()) {
@@ -627,7 +627,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
     }
     lpvar jl = -1;
     for (auto j : f ) {
-        if (abs(vvr(j)) == abs_mv) {
+        if (abs(val(j)) == abs_mv) {
             jl = var(j);
             break;
         }
@@ -639,7 +639,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
         if (var(j) == jl) {
             continue;
         }
-        if (abs(vvr(j)) != rational(1)) {
+        if (abs(val(j)) != rational(1)) {
             not_one_j = var(j);
             break;
         }
@@ -654,7 +654,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
     c().mk_ineq(mon_var, llc::EQ);
         
     // negate abs(jl) == abs()
-    if (vvr(jl) == - vvr(mon_var))
+    if (val(jl) == - val(mon_var))
         c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma());   
     else  // jl == mon_var
         c().mk_ineq(jl, -rational(1), mon_var, llc::NE);   
@@ -689,7 +689,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
     lpvar not_one = -1;
     for (auto j : f){
         TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout););
-        auto v = vvr(j);
+        auto v = val(j);
         if (v == rational(1)) {
             continue;
         }
@@ -710,13 +710,13 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
 
     if (not_one + 1) {
         // we found the only not_one
-        if (vvr(rm) == vvr(not_one) * sign) {
+        if (val(rm) == val(not_one) * sign) {
             TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
             return false;
         }
     } else {
         // we have +-ones only in the factorization
-        if (vvr(rm) == sign) {
+        if (val(rm) == sign) {
             return false;
         }
     }
@@ -728,7 +728,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
     for (auto j : f){
         lpvar var_j = var(j);
         if (not_one == var_j) continue;
-        c().mk_ineq(var_j, llc::NE, j.is_var()? vvr(j) : c().canonize_sign(j) * vvr(j));   
+        c().mk_ineq(var_j, llc::NE, j.is_var()? val(j) : c().canonize_sign(j) * val(j));   
     }
 
     if (not_one == static_cast<lpvar>(-1)) {
@@ -750,7 +750,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
     TRACE("nla_solver_bl", c().print_factorization(f, tout););
     int zero_j = -1;
     for (auto j : f) {
-        if (vvr(j).is_zero()) {
+        if (val(j).is_zero()) {
             zero_j = var(j);
             break;
         }
diff --git a/src/util/lp/nla_common.cpp b/src/util/lp/nla_common.cpp
index 40223ac66..d35b684b6 100644
--- a/src/util/lp/nla_common.cpp
+++ b/src/util/lp/nla_common.cpp
@@ -32,10 +32,10 @@ template void common::explain<factorization>(const factorization& t);
 
 void common::explain(lpvar j) { c().explain(j, c().current_expl()); }
 
-template <typename T> rational common::vvr(T const& t) const { return c().vvr(t); }
-template rational common::vvr<monomial>(monomial const& t) const;
-template rational common::vvr<factor>(factor const& t) const;
-rational common::vvr(lpvar t) const { return c().vvr(t); }
+template <typename T> rational common::val(T const& t) const { return c().val(t); }
+template rational common::val<monomial>(monomial const& t) const;
+template rational common::val<factor>(factor const& t) const;
+rational common::val(lpvar t) const { return c().val(t); }
 template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
 template lpvar common::var<factor>(factor const& t) const;
 template lpvar common::var<monomial>(monomial const& t) const;
diff --git a/src/util/lp/nla_common.h b/src/util/lp/nla_common.h
index 31703fb40..2c954aa8a 100644
--- a/src/util/lp/nla_common.h
+++ b/src/util/lp/nla_common.h
@@ -49,8 +49,8 @@ struct common {
     core& _() { return *m_core; }
     const core& _() const { return *m_core; }
 
-    template <typename T> rational vvr(T const& t) const;
-    rational vvr(lpvar) const;
+    template <typename T> rational val(T const& t) const;
+    rational val(lpvar) const;
     template <typename T> lpvar var(T const& t) const;
     bool done() const;
     template <typename T> void explain(const T&);
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index 92152acac..87faddbdd 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -48,7 +48,7 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
 rational core::value(const lp::lar_term& r) const {
     rational ret(0);
     for (const auto & t : r.coeffs()) {
-        ret += t.second * vvr(t.first);
+        ret += t.second * val(t.first);
     }
     return ret;
 }
@@ -151,7 +151,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
     bool first = true;
     for (lpvar v : m) {
         if (!first) out << "*"; else first = false;
-        out << "(" << m_lar_solver.get_variable_name(v) << "=" << vvr(v) << ")";
+        out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
     }
     return out;
 }
@@ -180,7 +180,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
 }
 
 std::ostream& core::print_monomial(const monomial& m, std::ostream& out) const {
-    out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << vvr(m.var()) << " = ";
+    out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
     print_product(m.vars(), out) << ")\n";
     return out;
 }
@@ -497,7 +497,7 @@ const lp::explanation& core::current_expl() const { return current_lemma().expl(
 int core::vars_sign(const svector<lpvar>& v) {
     int sign = 1;
     for (lpvar j : v) {
-        sign *= nla::rat_sign(vvr(j));
+        sign *= nla::rat_sign(val(j));
         if (sign == 0) 
             return 0;
     }
@@ -562,7 +562,7 @@ bool core::zero_is_an_inner_point_of_bounds(lpvar j) const {
 int core::rat_sign(const monomial& m) const {
     int sign = 1;
     for (lpvar j : m.vars()) {
-        auto v = vvr(j);
+        auto v = val(j);
         if (v.is_neg()) {
             sign = - sign;
             continue;
@@ -577,8 +577,8 @@ int core::rat_sign(const monomial& m) const {
 }
 
 // Returns true if the monomial sign is incorrect
-bool core:: sign_contradiction(const monomial& m) const {
-    return  nla::rat_sign(vvr(m)) != rat_sign(m);
+bool core::sign_contradiction(const monomial& m) const {
+    return  nla::rat_sign(val(m)) != rat_sign(m);
 }
 
 /*
@@ -718,7 +718,7 @@ std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
 std::ostream & core::print_var(lpvar j, std::ostream & out) const {
     if (m_emons.is_monomial_var(j)) {
         print_monomial(m_emons[j], out);
-        out << " = " << vvr(j);;
+        out << " = " << val(j);;
     }
         
     m_lar_solver.print_column_info(j, out) <<";";
@@ -791,8 +791,8 @@ void core::explain_existing_upper_bound(lpvar j) {
 }
     
 void core::explain_separation_from_zero(lpvar j) {
-    SASSERT(!vvr(j).is_zero());
-    if (vvr(j).is_pos())
+    SASSERT(!val(j).is_zero());
+    if (val(j).is_pos())
         explain_existing_lower_bound(j);
     else
         explain_existing_upper_bound(j);
@@ -816,7 +816,7 @@ void core::trace_print_monomial_and_factorization(const monomial& rm, const fact
     out << "\n";
         
     out << "mon:  " << pp_mon(*this, rm.var()) << "\n";
-    out << "value: " << vvr(rm) << "\n";
+    out << "value: " << val(rm) << "\n";
     print_factorization(f, out << "fact: ") << "\n";
 }
 
@@ -906,93 +906,14 @@ bool core:: basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const roo
         }
     }
 
-    if (not_one_j == static_cast<lpvar>(-1)) {
-        return false;
-    } 
-
-    add_empty_lemma();
-    // mon_var = 0
-    mk_ineq(mon_var, llc::EQ);
-        
-    // negate abs(jl) == abs()
-    if (vvr(jl) == - vvr(mon_var))
-        mk_ineq(jl, mon_var, llc::NE, current_lemma());   
-    else  // jl == mon_var
-        mk_ineq(jl, -rational(1), mon_var, llc::NE);   
-
-    // not_one_j = 1
-    mk_ineq(not_one_j, llc::EQ,  rational(1));   
-        
-    // not_one_j = -1
-    mk_ineq(not_one_j, llc::EQ, -rational(1));
-    explain(rm, current_expl());
-    explain(f, current_expl());
-
-    TRACE("nla_solver", print_lemma(tout); );
-    return true;
-}
-// use the fact that
-// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-bool core:: basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m) {
-    TRACE("nla_solver_bl", print_monomial(m, tout););
-
-    lpvar mon_var = m.var();
-    const auto & mv = vvr(mon_var);
-    const auto  abs_mv = abs(mv);
-    if (abs_mv == rational::zero()) {
-        return false;
-    }
-    lpvar jl = -1;
-    for (auto j : m ) {
-        if (abs(vvr(j)) == abs_mv) {
-            jl = j;
-            break;
-        }
-    }
-    if (jl == static_cast<lpvar>(-1))
-        return false;
-    lpvar not_one_j = -1;
-    for (auto j : m ) {
-        if (j == jl) {
-            continue;
-        }
-        if (abs(vvr(j)) != rational(1)) {
-            not_one_j = j;
-            break;
-        }
-    }
-
-    if (not_one_j == static_cast<lpvar>(-1)) {
-        return false;
-    } 
-
-    add_empty_lemma();
-    // mon_var = 0
-    mk_ineq(mon_var, llc::EQ);
-        
-    // negate abs(jl) == abs()
-    if (vvr(jl) == - vvr(mon_var))
-        mk_ineq(jl, mon_var, llc::NE, current_lemma());   
-    else  // jl == mon_var
-        mk_ineq(jl, -rational(1), mon_var, llc::NE);   
-
-    // not_one_j = 1
-    mk_ineq(not_one_j, llc::EQ,  rational(1));   
-        
-    // not_one_j = -1
-    mk_ineq(not_one_j, llc::EQ, -rational(1));
-    TRACE("nla_solver", print_lemma(tout); );
-    return true;
-}
-
-bool core:: vars_are_equiv(lpvar a, lpvar b) const {
-    SASSERT(abs(vvr(a)) == abs(vvr(b)));
+bool core::vars_are_equiv(lpvar a, lpvar b) const {
+    SASSERT(abs(val(a)) == abs(val(b)));
     return m_evars.vars_are_equiv(a, b);
 }
 
     
 void core::explain_equiv_vars(lpvar a, lpvar b) {
-    SASSERT(abs(vvr(a)) == abs(vvr(b)));
+    SASSERT(abs(val(a)) == abs(val(b)));
     if (m_evars.vars_are_equiv(a, b)) {
         explain(a, current_expl());
         explain(b, current_expl());
@@ -1245,7 +1166,7 @@ void core::explain(const factorization& f, lp::explanation& exp) {
 
 bool core:: has_zero_factor(const factorization& factorization) const {
     for (factor f : factorization) {
-        if (vvr(f).is_zero())
+        if (val(f).is_zero())
             return true;
     }
     return false;
@@ -1255,7 +1176,7 @@ bool core:: has_zero_factor(const factorization& factorization) const {
 template <typename T>
 bool core:: mon_has_zero(const T& product) const {
     for (lpvar j: product) {
-        if (vvr(j).is_zero())
+        if (val(j).is_zero())
             return true;
     }
     return false;
@@ -1292,7 +1213,7 @@ void core::collect_equivs_of_fixed_vars() {
     for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
         if (!var_is_fixed(j))
             continue;
-        rational v = abs(vvr(j));
+        rational v = abs(val(j));
         auto it = abs_map.find(v);
         if (it == abs_map.end()) {
             abs_map[v] = svector<lpvar>();
@@ -1309,10 +1230,10 @@ void core::collect_equivs_of_fixed_vars() {
         for (unsigned k = 1; k < v.size(); k++) {
             auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]);
             auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]);
-            if (vvr(head) == vvr(v[k])) {
+            if (val(head) == val(v[k])) {
                 m_evars.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3}));
             } else {
-                SASSERT(vvr(head) == -vvr(v[k]));
+                SASSERT(val(head) == -val(v[k]));
                 m_evars.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3}));
             }
         }
@@ -1396,7 +1317,7 @@ void core::print_monomial_stats(const monomial& m, std::ostream& out) {
     if (m.size() == 2) return;
     monomial_coeff mc = canonize_monomial(m);
     for(unsigned i = 0; i < mc.vars().size(); i++){
-        if (abs(vvr(mc.vars()[i])) == rational(1)) {
+        if (abs(val(mc.vars()[i])) == rational(1)) {
             auto vv = mc.vars();
             vv.erase(vv.begin()+i);
             monomial const* sv = m_emons.find_canonical(vv);
@@ -1488,7 +1409,7 @@ void core::negate_factor_equality(const factor& c,
         return;
     lpvar i = var(c);
     lpvar j = var(d);
-    auto iv = vvr(i), jv = vvr(j);
+    auto iv = val(i), jv = val(j);
     SASSERT(abs(iv) == abs(jv));
     if (iv == jv) {
         mk_ineq(i, -rational(1), j, llc::NE);
@@ -1500,7 +1421,7 @@ void core::negate_factor_equality(const factor& c,
 void core::negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) {
     rational a_fs = canonize_sign(a);
     rational b_fs = canonize_sign(b);
-    llc cmp = a_sign*vvr(a) < b_sign*vvr(b)? llc::GE : llc::LE;
+    llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
     mk_ineq(a_fs*a_sign, var(a), - b_fs*b_sign, var(b), cmp);
 }
 
@@ -1543,7 +1464,7 @@ void core::maybe_add_a_factor(lpvar i,
                               std::unordered_set<lpvar>& found_vars,
                               std::unordered_set<unsigned>& found_rm,
                               vector<factor> & r) const {
-    SASSERT(abs(vvr(i)) == abs(vvr(c)));
+    SASSERT(abs(val(i)) == abs(val(c)));
     if (!m_emons.is_monomial_var(i)) {
         i = m_evars.find(i).var();
         if (try_insert(i, found_vars)) {
@@ -1583,30 +1504,30 @@ bool core::rm_check(const monomial& rm) const {
 /**
    \brief Add |v| ~ |bound|
    where ~ is <, <=, >, >=, 
-   and bound = vvr(v)
+   and bound = val(v)
 
    |v| > |bound| 
    <=> 
    (v < 0 or v > |bound|) & (v > 0 or -v > |bound|)        
-   => Let s be the sign of vvr(v)
+   => Let s be the sign of val(v)
    (s*v < 0 or s*v > |bound|)         
 
    |v| < |bound|
    <=>
    v < |bound| & -v < |bound| 
-   => Let s be the sign of vvr(v)
+   => Let s be the sign of val(v)
    s*v < |bound|
 
 */
 
 void core::add_abs_bound(lpvar v, llc cmp) {
-    add_abs_bound(v, cmp, vvr(v));
+    add_abs_bound(v, cmp, val(v));
 }
 
 void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
-    SASSERT(!vvr(v).is_zero());
+    SASSERT(!val(v).is_zero());
     lp::lar_term t;  // t = abs(v)
-    t.add_coeff_var(rrat_sign(vvr(v)), v);
+    t.add_coeff_var(rrat_sign(val(v)), v);
 
     switch (cmp) {
     case llc::GT:
@@ -1626,9 +1547,9 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
 // NB - move this comment to monotonicity or appropriate.
 /** \brief enforce the inequality |m| <= product |m[i]| .
     by enforcing lemma:
-    /\_i |m[i]| <= |vvr(m[i])| => |m| <= |product_i vvr(m[i])|
+    /\_i |m[i]| <= |val(m[i])| => |m| <= |product_i val(m[i])|
     <=>
-    \/_i |m[i]| > |vvr(m[i])} or |m| <= |product_i vvr(m[i])|
+    \/_i |m[i]| > |val(m[i])} or |m| <= |product_i val(m[i])|
 */
 
     
@@ -1637,7 +1558,7 @@ bool core::find_bfc_to_refine_on_rmonomial(const monomial& rm, bfc & bf) {
         if (factorization.size() == 2) {
             auto a = factorization[0];
             auto b = factorization[1];
-            if (vvr(rm) != vvr(a) * vvr(b)) {
+            if (val(rm) != val(a) * val(b)) {
                 bf = bfc(a, b);
                 return true;
             }
@@ -1668,7 +1589,7 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
             TRACE("nla_solver", tout << "found bf";
                   tout << ":rm:" << rm << "\n";
                   tout << "bf:"; print_bfc(bf, tout);
-                  tout << ", product = " << vvr(rm) << ", but should be =" << vvr(bf.m_x)*vvr(bf.m_y);
+                  tout << ", product = " << val(rm) << ", but should be =" << val(bf.m_x)*val(bf.m_y);
                   tout << ", j == "; print_var(j, tout) << "\n";);
             return true;
         } 
@@ -1679,10 +1600,10 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
 void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
     SASSERT(sign == nla::rat_sign(product_value(m.vars())));
     for (lpvar j : m.vars()) {
-        if (vvr(j).is_pos()) {
+        if (val(j).is_pos()) {
             mk_ineq(j, llc::LE);
         } else {
-            SASSERT(vvr(j).is_neg());
+            SASSERT(val(j).is_neg());
             mk_ineq(j, llc::GE);
         }
     }
@@ -1805,8 +1726,8 @@ void core::generate_tang_plane(const rational & a, const rational& b, const fact
 }  
 
 void core::negate_relation(unsigned j, const rational& a) {
-    SASSERT(vvr(j) != a);
-    if (vvr(j) < a) {
+    SASSERT(val(j) != a);
+    if (val(j) < a) {
         mk_ineq(j, llc::GE, a);
     }
     else {
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index dadd8fa14..5a40e3bb6 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -96,17 +96,15 @@ public:
     bool ineq_holds(const ineq& n) const;
     bool lemma_holds(const lemma& l) const;
   
-    rational vvr(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
+    rational val(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
 
-    rational vvr(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
+    rational val(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
 
-    lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
-    
     lpvar var(monomial const& sv) const { return sv.var(); }
 
-    rational vvr_rooted(const monomial& m) const { return m.rsign()*vvr(m.var()); }
+    rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); }
 
-    rational vvr(const factor& f) const {  return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
+    rational val(const factor& f) const {  return f.is_var()? val(f.var()) : val(m_emons[f.var()]); }
 
     lpvar var(const factor& f) const { return f.var(); }
 
@@ -227,7 +225,7 @@ public:
     bool zero_is_an_inner_point_of_bounds(lpvar j) const;
     
     int rat_sign(const monomial& m) const;
-    inline int rat_sign(lpvar j) const { return nla::rat_sign(vvr(j)); }
+    inline int rat_sign(lpvar j) const { return nla::rat_sign(val(j)); }
 
     bool sign_contradiction(const monomial& m) const;
 
diff --git a/src/util/lp/nla_monotone_lemmas.cpp b/src/util/lp/nla_monotone_lemmas.cpp
index 0fa9e72e5..d1d2bf031 100644
--- a/src/util/lp/nla_monotone_lemmas.cpp
+++ b/src/util/lp/nla_monotone_lemmas.cpp
@@ -36,9 +36,9 @@ void monotone::monotonicity_lemma() {
 
 
 void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
-    rational av = vvr(a);
+    rational av = val(a);
     rational as = rational(nla::rat_sign(av));
-    rational bv = vvr(b);
+    rational bv = val(b);
     rational bs = rational(nla::rat_sign(bv));
     TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";);
     SASSERT(as*av <= bs*bv);
@@ -56,9 +56,9 @@ void monotone::assert_abs_val_a_le_abs_var_b(
     bool strict) {
     lpvar aj = var(a);
     lpvar bj = var(b);
-    rational av = vvr(aj);
+    rational av = val(aj);
     rational as = rational(nla::rat_sign(av));
-    rational bv = vvr(bj);
+    rational bv = val(bj);
     rational bs = rational(nla::rat_sign(bv));
     //        TRACE("nla_solver", tout << "rmv = " << rmv << ", jv = " << jv << "\n";);
     mk_ineq(as, aj, llc::LT); // |aj| < 0
@@ -67,9 +67,9 @@ void monotone::assert_abs_val_a_le_abs_var_b(
 }
 
 void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
-    rational av = vvr(a);
+    rational av = val(a);
     rational as = rational(nla::rat_sign(av));
-    rational bv = vvr(b);
+    rational bv = val(b);
     rational bs = rational(nla::rat_sign(bv));
     TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";);
     SASSERT(as*av < bs*bv);
@@ -83,7 +83,7 @@ void monotone::monotonicity_lemma(monomial const& m) {
     if (c().mon_has_zero(m.vars()))
         return;
     const rational prod_val = abs(c().product_value(m.vars()));
-    const rational m_val = abs(vvr(m));
+    const rational m_val = abs(val(m));
     if (m_val < prod_val)
         monotonicity_lemma_lt(m, prod_val);
     else if (m_val > prod_val)
@@ -102,9 +102,9 @@ void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val
     
 /** \brief enforce the inequality |m| >= product |m[i]| .
 
-    /\_i |m[i]| >= |vvr(m[i])| => |m| >= |product_i vvr(m[i])|
+    /\_i |m[i]| >= |val(m[i])| => |m| >= |product_i val(m[i])|
     <=>
-    \/_i |m[i]| < |vvr(m[i])} or |m| >= |product_i vvr(m[i])|
+    \/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])|
 */
 void monotone::monotonicity_lemma_lt(const monomial& m, const rational& prod_val) {
     add_empty_lemma();
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index e8101fcc3..87f384ed4 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -63,8 +63,8 @@ void order::order_lemma_on_rmonomial(const monomial& m) {
 void order::order_lemma_on_binomial(const monomial& ac) {
     TRACE("nla_solver", tout << pp_mon(c(), ac););
     SASSERT(!check_monomial(ac) && ac.size() == 2);
-    const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]);
-    const rational acv = vvr(ac);
+    const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]);
+    const rational acv = val(ac);
     bool gt = acv > mult_val;
     bool k = false;
     do {
@@ -75,13 +75,13 @@ void order::order_lemma_on_binomial(const monomial& ac) {
 }
 
 void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
-    SASSERT(gt == (vvr(m) > vvr(m.vars()[0]) * vvr(m.vars()[1])));
+    SASSERT(gt == (val(m) > val(m.vars()[0]) * val(m.vars()[1])));
     order_lemma_on_binomial_sign(m, m.vars()[k], m.vars()[!k], gt ? 1: -1);
 }
 
 /**
 \brief
- sign = the sign of vvr(xy) - vvr(x) * vvr(y) != 0
+ sign = the sign of val(xy) - val(x) * val(y) != 0
  y <= 0 or x < a or xy >= ay
  y <= 0 or x > a or xy <= ay
  y >= 0 or x < a or xy <= ay
@@ -90,11 +90,11 @@ void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
 */
 void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, int sign) {
     SASSERT(!_().mon_has_zero(xy.vars()));
-    int sy = rat_sign(vvr(y));
+    int sy = rat_sign(val(y));
     add_empty_lemma();
     mk_ineq(y,                     sy == 1      ? llc::LE : llc::GE); // negate sy
-    mk_ineq(x,                     sy*sign == 1 ? llc::GT : llc::LT , vvr(x)); 
-    mk_ineq(xy.var(), - vvr(x), y, sign == 1    ? llc::LE : llc::GE);
+    mk_ineq(x,                     sy*sign == 1 ? llc::GT : llc::LT , val(x)); 
+    mk_ineq(xy.var(), - val(x), y, sign == 1    ? llc::LE : llc::GE);
     TRACE("nla_solver", print_lemma(tout););
 }
 // m's size is 2 and m = m[k]a[!k] if k is false and m = m[!k]a[k] if k is true
@@ -127,12 +127,12 @@ void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const mono
     lpvar a = ac.vars()[p];
     lpvar c = ac.vars()[k];
     SASSERT(_().m_evars.find(c).var() == d);
-    rational acv = vvr(ac);
-    rational av = vvr(a);
-    rational c_sign = rrat_sign(vvr(c));
-    rational d_sign = rrat_sign(vvr(d));
-    rational bdv = vvr(bd);
-    rational bv = vvr(b);
+    rational acv = val(ac);
+    rational av = val(a);
+    rational c_sign = rrat_sign(val(c));
+    rational d_sign = rrat_sign(val(d));
+    rational bdv = val(bd);
+    rational bv = val(b);
     auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
 
     // suppose ac >= bd, then ac/|c| >= bd/|d|.
@@ -193,11 +193,11 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
     rational sign = m.rsign();
     for (factor f: ab)
         sign *= _().canonize_sign(f);
-    const rational fv = vvr(ab[0]) * vvr(ab[1]);
-    const rational mv = sign * vvr(m);
+    const rational fv = val(ab[0]) * val(ab[1]);
+    const rational mv = sign * val(m);
     TRACE("nla_solver",
           tout << "ab.size()=" << ab.size() << "\n";
-          tout << "we should have sign*vvr(m):" << mv << "=(" << sign << ")*(" << vvr(m) <<") to be equal to " << " vvr(ab[0])*vvr(ab[1]):" << fv << "\n";);
+          tout << "we should have sign*val(m):" << mv << "=(" << sign << ")*(" << val(m) <<") to be equal to " << " val(ab[0])*val(ab[1]):" << fv << "\n";);
     if (mv == fv)
         return;
     bool gt = mv > fv;
@@ -256,7 +256,7 @@ void order::generate_ol(const monomial& ac,
 
 void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b) {
     rational b_fs = canonize_sign(b);
-    llc cmp = a_sign*vvr(a) < b_sign*vvr(b)? llc::GE : llc::LE;
+    llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
     mk_ineq(a_sign, a, - b_fs*b_sign, var(b), cmp);
 }
 
@@ -266,13 +266,13 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
                                                  const factor& c,
                                                  const monomial& bc,
                                                  const factor& b) {
-    auto cv = vvr(c); 
+    auto cv = val(c); 
     int c_sign = nla::rat_sign(cv);
     SASSERT(c_sign != 0);
-    auto av_c_s = vvr(a)*rational(c_sign);
-    auto bv_c_s = vvr(b)*rational(c_sign);        
-    auto acv = vvr(ac); 
-    auto bcv = vvr(bc); 
+    auto av_c_s = val(a)*rational(c_sign);
+    auto bv_c_s = val(b)*rational(c_sign);        
+    auto acv = val(ac); 
+    auto bcv = val(bc); 
     TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
     // Suppose ac >= bc, then ac/|c| >= bc/|c|.
     // Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s
@@ -291,51 +291,51 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
    a < 0 & b >= value(b) => sign*ab <= value(b)*a  if value(a) < 0
 */
 void order::order_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar a, lpvar b) {
-    SASSERT(sign * vvr(m) > vvr(a) * vvr(b));
+    SASSERT(sign * val(m) > val(a) * val(b));
     add_empty_lemma();
-    if (vvr(a).is_pos()) {
+    if (val(a).is_pos()) {
         TRACE("nla_solver", tout << "a is pos\n";);
         //negate a > 0
         mk_ineq(a, llc::LE);
-        // negate b <= vvr(b)
-        mk_ineq(b, llc::GT, vvr(b));
-        // ab <= vvr(b)a
-        mk_ineq(sign, m.var(), -vvr(b), a, llc::LE);
+        // negate b <= val(b)
+        mk_ineq(b, llc::GT, val(b));
+        // ab <= val(b)a
+        mk_ineq(sign, m.var(), -val(b), a, llc::LE);
     } else {
         TRACE("nla_solver", tout << "a is neg\n";);
-        SASSERT(vvr(a).is_neg());
+        SASSERT(val(a).is_neg());
         //negate a < 0
         mk_ineq(a, llc::GE);
-        // negate b >= vvr(b)
-        mk_ineq(b, llc::LT, vvr(b));
-        // ab <= vvr(b)a
-        mk_ineq(sign, m.var(), -vvr(b), a, llc::LE);
+        // negate b >= val(b)
+        mk_ineq(b, llc::LT, val(b));
+        // ab <= val(b)a
+        mk_ineq(sign, m.var(), -val(b), a, llc::LE);
     }
 }
-// we need to deduce ab >= vvr(b)*a
+// we need to deduce ab >= val(b)*a
 /**
    \brief Add lemma: 
    a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0
    a < 0 & b <= value(b) => sign*ab >= value(b)*a if value(a) < 0
 */
 void order::order_lemma_on_ab_lt(const monomial& m, const rational& sign, lpvar a, lpvar b) {
-    SASSERT(sign * vvr(m) < vvr(a) * vvr(b));
+    SASSERT(sign * val(m) < val(a) * val(b));
     add_empty_lemma();
-    if (vvr(a).is_pos()) {
+    if (val(a).is_pos()) {
         //negate a > 0
         mk_ineq(a, llc::LE);
-        // negate b >= vvr(b)
-        mk_ineq(b, llc::LT, vvr(b));
-        // ab <= vvr(b)a
-        mk_ineq(sign, m.var(), -vvr(b), a, llc::GE);
+        // negate b >= val(b)
+        mk_ineq(b, llc::LT, val(b));
+        // ab <= val(b)a
+        mk_ineq(sign, m.var(), -val(b), a, llc::GE);
     } else {
-        SASSERT(vvr(a).is_neg());
+        SASSERT(val(a).is_neg());
         //negate a < 0
         mk_ineq(a, llc::GE);
-        // negate b <= vvr(b)
-        mk_ineq(b, llc::GT, vvr(b));
-        // ab >= vvr(b)a
-        mk_ineq(sign, m.var(), -vvr(b), a, llc::GE);
+        // negate b <= val(b)
+        mk_ineq(b, llc::GT, val(b));
+        // ab >= val(b)a
+        mk_ineq(sign, m.var(), -val(b), a, llc::GE);
     }
 }
 
diff --git a/src/util/lp/nla_order_lemmas.h b/src/util/lp/nla_order_lemmas.h
index 9ccb66b11..fa307d146 100644
--- a/src/util/lp/nla_order_lemmas.h
+++ b/src/util/lp/nla_order_lemmas.h
@@ -55,7 +55,7 @@ private:
        a < 0 & b >= value(b) => sign*ab <= value(b)*a  if value(a) < 0
     */
     void order_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar a, lpvar b);
-    // we need to deduce ab >= vvr(b)*a
+    // we need to deduce ab >= val(b)*a
     /**
        \brief Add lemma: 
        a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0
diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp
index 5d44eaa49..479a7e1e9 100644
--- a/src/util/lp/nla_tangent_lemmas.cpp
+++ b/src/util/lp/nla_tangent_lemmas.cpp
@@ -21,7 +21,7 @@
 #include "util/lp/nla_core.h"
 
 namespace nla {
-template <typename T> rational tangents::vvr(T const& t) const { return m_core->vvr(t); }
+template <typename T> rational tangents::val(T const& t) const { return m_core->val(t); }
 
 tangents::tangents(core * c) : common(c) {}
 
@@ -36,7 +36,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
     TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
     c().add_empty_lemma();
     const rational v = c().product_value(m.vars());
-    const rational mv = vvr(m);
+    const rational mv = val(m);
     SASSERT(mv != v);
     SASSERT(!mv.is_zero() && !v.is_zero());
     rational sign = rational(nla::rat_sign(mv));
@@ -47,7 +47,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
     bool gt = abs(mv) > abs(v);
     if (gt) {
         for (lpvar j : m.vars()) {
-            const rational jv = vvr(j);
+            const rational jv = val(j);
             rational js = rational(nla::rat_sign(jv));
             c().mk_ineq(js, j, llc::LT);
             c().mk_ineq(js, j, llc::GT, jv);
@@ -55,7 +55,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
         c().mk_ineq(sign, m.var(), llc::LE, std::max(v, rational(-1)));
     } else {
         for (lpvar j : m.vars()) {
-            const rational jv = vvr(j);
+            const rational jv = val(j);
             rational js = rational(nla::rat_sign(jv));
             c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0)));
         }
@@ -95,11 +95,11 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
     c().negate_relation(jy, b);
     bool sbelow = j_sign.is_pos()? below: !below;
 #if Z3DEBUG
-    int mult_sign = nla::rat_sign(a - vvr(jx))*nla::rat_sign(b - vvr(jy));
+    int mult_sign = nla::rat_sign(a - val(jx))*nla::rat_sign(b - val(jy));
     SASSERT((mult_sign == 1) == sbelow);
     // If "mult_sign is 1"  then (a - x)(b-y) > 0 and ab - bx - ay + xy > 0
     // or -ab + bx + ay < xy or -ay - bx + xy > -ab
-    // j_sign*vvr(j) stands for xy. So, finally we have  -ay - bx + j_sign*j > - ab
+    // j_sign*val(j) stands for xy. So, finally we have  -ay - bx + j_sign*j > - ab
 #endif
 
     lp::lar_term t;
@@ -110,12 +110,12 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
 }  
 void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const monomial* rm){
     point a, b;
-    point xy (vvr(bf.m_x), vvr(bf.m_y));
+    point xy (val(bf.m_x), val(bf.m_y));
     rational correct_mult_val =  xy.x * xy.y;
-    rational val = vvr(j) * sign;
-    bool below = val < correct_mult_val;
+    rational v = val(j) * sign;
+    bool below = v < correct_mult_val;
     TRACE("nla_solver", tout << "rm = " << rm << ", below = " << below << std::endl; );
-    get_tang_points(a, b, below, val, xy);
+    get_tang_points(a, b, below, v, xy);
     TRACE("nla_solver", tout << "sign = " << sign << ", tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;);
     unsigned lemmas_size_was = c().m_lemma_vec->size();
     generate_two_tang_lines(bf, xy, sign, j);
diff --git a/src/util/lp/nla_tangent_lemmas.h b/src/util/lp/nla_tangent_lemmas.h
index e5ac673c6..c2e608a3c 100644
--- a/src/util/lp/nla_tangent_lemmas.h
+++ b/src/util/lp/nla_tangent_lemmas.h
@@ -80,7 +80,7 @@ private:
                                const rational & correct_val,                             
                                const rational & val,
                                bool below) const;
-    template <typename T> rational vvr(T const& t) const;
+    template <typename T> rational val(T const& t) const;
     template <typename T> lpvar var(T const& t) const { return t.var(); }
 }; // end of tangents
 }
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index 6173a115b..ca4f51a94 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -64,11 +64,11 @@ struct vars_equivalence {
     // If m_tree[v] == -1 then the variable is a root.
     // if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v
     vector<equiv>                                 m_equivs;         // all equivalences extracted from constraints
-    std::function<rational(lpvar)>                m_vvr;
+    std::function<rational(lpvar)>                m_val;
     
 
     // constructor
-    vars_equivalence(std::function<rational(lpvar)> vvr) : m_vvr(vvr) {}
+    vars_equivalence(std::function<rational(lpvar)> val) : m_val(val) {}
     
     void clear() {
         m_equivs.clear();