diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 1ea87251705..58c24f2ca3b 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -146,7 +146,7 @@ class lp_bound_propagator {
         unsigned v_j = v->column();
         unsigned j = null_lpvar;
         if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
-            // try_add_equation_with_internal_fixed_tables(row_index, v);
+            try_add_equation_with_internal_fixed_tables(row_index, v);
             return;
         }
        
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0abc2870db1..88fdb3d8849 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2084,7 +2084,7 @@ class theory_lra::imp {
         while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
             auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
             
-            m_bv_to_propagate.push_back(bv);
+            // m_bv_to_propagate.push_back(bv);
             
             api_bound* b = nullptr;
             TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";