diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8ffeff3fb..8bf17ec4d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1529,12 +1529,10 @@ public: 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 @@ public: } } - 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)); }