diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 76f8f8096..383c63b8f 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -346,11 +346,6 @@ namespace sls {
             SASSERT(dtt(sign(bv), ineq) == 0);
         }
         vi.m_value = new_value;
-        if (vi.m_shared) {
-            sort* s = vi.m_sort == var_sort::INT ? a.mk_int() : a.mk_real();
-            expr_ref num = from_num(s, new_value);
-            ctx.set_value(vi.m_expr, num);
-        }
         for (auto idx : vi.m_muls) {
             auto const& [w, coeff, monomial] = m_muls[idx];
             ctx.new_value_eh(m_vars[w].m_expr);
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index 54233ec59..93b5b717d 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -67,7 +67,6 @@ namespace sls {
             expr*        m_expr;
             num_t        m_value{ 0 };
             num_t        m_best_value{ 0 };
-            bool         m_shared = false;
             var_sort     m_sort;
             arith_op_kind m_op = arith_op_kind::LAST_ARITH_OP;
             unsigned     m_def_idx = UINT_MAX;