#5614 turn on / off options to get better performance.

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 12, 2021 · 63ac2ee · 63ac2ee
1 parent b28a801
commit 63ac2ee
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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";