diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index e5e7fcc76..925948e4a 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -76,7 +76,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 = vvr(j);
     if (v.is_zero()) {
         try_get_non_strict_sign_from_bounds(j, sign);
     } else {
@@ -323,8 +323,8 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon&
     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  abs_mv = abs(mv);
+    const auto mv = vvr(mon_var);
+    const auto abs_mv = abs(mv);
         
     if (abs_mv == rational::zero()) {
         return false;
@@ -570,8 +570,8 @@ 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  abs_mv = abs(mv);
+    const auto mv = vvr(mon_var);
+    const auto abs_mv = abs(mv);
     if (abs_mv == rational::zero()) {
         return false;
     }
@@ -670,8 +670,8 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const sm
     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  abs_mv = abs(mv);
+    const auto mv = vvr(mon_var);
+    const auto abs_mv = abs(mv);
         
     if (abs_mv == rational::zero()) {
         return false;
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 477ea8094..f6b828990 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -54,7 +54,7 @@ void order::order_lemma_on_rmonomial(const smon& rm) {
 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[0]) * vvr(ac[1]);
+    const rational mult_val = vvr(ac[0]) * vvr(ac[1]);
     const rational acv = vvr(ac);
     bool gt = acv > mult_val;
     for (unsigned k = 0; k < 2; k++) {
@@ -182,7 +182,7 @@ void order::order_lemma_on_factorization(const smon& rm, const factorization& ab
     rational sign = _().m_emons.orig_sign(rm);
     for (factor f: ab)
         sign *= _().canonize_sign(f);
-    const rational & fv = vvr(ab[0]) * vvr(ab[1]);
+    const rational fv = vvr(ab[0]) * vvr(ab[1]);
     const rational mv = sign * vvr(m);
     TRACE("nla_solver",
           tout << "ab.size()=" << ab.size() << "\n";
diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp
index f7d428992..4e7be8dac 100644
--- a/src/util/lp/nla_tangent_lemmas.cpp
+++ b/src/util/lp/nla_tangent_lemmas.cpp
@@ -40,7 +40,7 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
     m_core->add_empty_lemma();
     const monomial & m = c().m_emons[rm->var()];
     const rational v = c().product_value(m);
-    const rational& mv = vvr(m);
+    const rational mv = vvr(m);
     SASSERT(mv != v);
     SASSERT(!mv.is_zero() && !v.is_zero());
     rational sign = rational(nla::rat_sign(mv));
@@ -51,7 +51,7 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
     bool gt = abs(mv) > abs(v);
     if (gt) {
         for (lpvar j : m) {
-            const rational & jv = vvr(j);
+            const rational jv = vvr(j);
             rational js = rational(nla::rat_sign(jv));
             c().mk_ineq(js, j, llc::LT);
             c().mk_ineq(js, j, llc::GT, jv);
@@ -59,7 +59,7 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
         c().mk_ineq(sign, rm->var(), llc::LE, std::max(v, rational(-1)));
     } else {
         for (lpvar j : m) {
-            const rational & jv = vvr(j);
+            const rational jv = vvr(j);
             rational js = rational(nla::rat_sign(jv));
             c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0)));
         }