diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 5ed9b4538..23d4016bd 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -95,7 +95,7 @@ namespace nla {
 
     scoped_anum& solver::tmp2() {
         SASSERT(use_nra_model());
-        return m_core->m_nra.tmp1();
+        return m_core->m_nra.tmp2();
     }
 
     
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 537291280..a32a4e964 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -918,7 +918,7 @@ namespace arith {
             theory_var v = (i + start) % sz;
             if (is_bool(v))
                 continue;
-            if (!ctx.is_shared(var2enode(v)) && !include_func_interp(var2enode(v)))
+            if (!ctx.is_shared(var2enode(v)))
                 continue;
             ensure_column(v);
             if (!is_registered_var(v))
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index bbe29da74..8669a514c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1513,7 +1513,7 @@ public:
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
-            if (!th.is_relevant_and_shared(n1) && !include_func_interp(n1))                     
+            if (!th.is_relevant_and_shared(n1))                   
                 continue;
             ensure_column(v);
             if (!is_registered_var(v))