diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 44c935330..60d65c5a6 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -1436,13 +1436,6 @@ namespace sls {
             for (auto const& [coeff, bv] : ui.m_linear_occurs)
                 vi.m_bool_vars_of.insert(bv);
         }
-        ;
-        for (auto bv : vi.m_bool_vars_of) {
-            for (auto i : ctx.get_use_list(sat::literal(bv, true)))
-                vi.m_clauses_of.insert(i);
-            for (auto i : ctx.get_use_list(sat::literal(bv, false)))
-                vi.m_clauses_of.insert(i);
-        }
     }
 
     template<typename num_t>
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index d073bf9bf..2c7cf0c7f 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -120,7 +120,6 @@ namespace sls {
             unsigned     m_def_idx = UINT_MAX;
             vector<std::pair<num_t, sat::bool_var>> m_linear_occurs;
             indexed_uint_set m_bool_vars_of;
-            indexed_uint_set m_clauses_of;
             unsigned_vector m_muls;
             unsigned_vector m_adds;
             optional<bound> m_lo, m_hi;
diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index bd3f0df99..8acdeeb77 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -286,32 +286,38 @@ namespace sls {
         if (!a.update_num(v, delta))
             return -1;
         double score = 0;
-        for (auto ci : vi.m_clauses_of) {
-            auto const& c = ctx.get_clause(ci);
-            unsigned num_true = 0;
-            for (auto lit : c) {
-                auto bv = lit.var();
-                auto ineq = a.get_ineq(bv);
-                if (ineq) {
-                    if (ineq->is_true() != lit.sign())
-                        ++num_true;
+        for (auto bv : vi.m_bool_vars_of) {
+            for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
+                for (auto ci : ctx.get_use_list(lit)) {
+                    auto const& c = ctx.get_clause(ci);
+                    unsigned num_true = 0;
+                    for (auto lit : c) {
+                        auto bv = lit.var();
+                        auto ineq = a.get_ineq(bv);
+                        if (ineq) {
+                            if (ineq->is_true() != lit.sign())
+                                ++num_true;
+                        }
+                        else if (ctx.is_true(lit))
+                            ++num_true;
+                    }
+
+                    CTRACE("arith_verbose", c.m_num_trues != num_true && (c.m_num_trues == 0 || num_true == 0),
+                        tout << "clause: " << c
+                        << " v" << v << " += " << delta
+                        << " new-true lits: " << num_true
+                        << " old-true lits: " << c.m_num_trues
+                        << " w: " << c.m_weight << "\n";
+                    for (auto lit : c)
+                        if (a.get_ineq(lit.var()))
+                            tout << lit << " " << *a.get_ineq(lit.var()) << "\n";);
+                    if (c.m_num_trues > 0 && num_true == 0)
+                        score -= c.m_weight;
+                    else if (c.m_num_trues == 0 && num_true > 0)
+                        score += c.m_weight;
                 }
-                else if (ctx.is_true(lit))
-                    ++num_true;
             }
-            CTRACE("arith_verbose", c.m_num_trues != num_true && (c.m_num_trues == 0 || num_true == 0),
-                tout << "clause: " << c
-                << " v" << v << " += " << delta
-                << " new-true lits: " << num_true
-                << " old-true lits: " << c.m_num_trues
-                << " w: " << c.m_weight << "\n";
-            for (auto lit : c) 
-                if (a.get_ineq(lit.var()))
-                    tout << lit << " " << *a.get_ineq(lit.var()) << "\n";);
-            if (c.m_num_trues > 0 && num_true == 0) 
-                score -= c.m_weight;            
-            else if (c.m_num_trues == 0 && num_true > 0) 
-                score += c.m_weight;            
+            
         }
 
         // revert the update
@@ -336,7 +342,6 @@ namespace sls {
             else
                 vi.set_value(num_t(0));
             vi.m_bool_vars_of.reset();
-            vi.m_clauses_of.reset();
         }
         initialize();
     }