rmove debug out

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 23, 2023 · 421fe94 · 421fe94
1 parent 886d3f4
commit 421fe94
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1529,12 +1529,10 @@ class theory_lra::imp {
         unsigned old_sz = m_assume_eq_candidates.size();
         unsigned num_candidates = 0;
         int start = ctx().get_random_value();
-        verbose_stream() << "assume-eqs " << sz << "\n";
         unsigned num_relevant = 0;
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
-            verbose_stream() << enode_pp(n1, ctx()) << "\n";
             if (!th.is_relevant_and_shared(n1)) {                    
                 continue;
             }
@@ -1557,7 +1555,6 @@ class theory_lra::imp {
             }
         }
 
-        verbose_stream() << "candidates " << num_candidates << " num relevant " << num_relevant << "\n";
         if (num_candidates > 0) {
             ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
         }