mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 06:01:26 +00:00
Code Activity

remove debug out from euf-completion

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-11-07 08:06:13 -08:00
parent f4c5e14b6b
commit 9f848847c7
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/simplifiers/euf_completion.cpp
View file

@ -806,7 +806,6 @@ namespace euf {
// callback when mam finds a binding // callback when mam finds a binding
void completion::on_binding(quantifier* q, app* pat, enode* const* binding, unsigned max_global, unsigned min_top, unsigned max_top) { void completion::on_binding(quantifier* q, app* pat, enode* const* binding, unsigned max_global, unsigned min_top, unsigned max_top) {
verbose_stream() << "on-binding\n";
if (should_stop()) if (should_stop())
return; return;
if (max_top >= m_max_generation) if (max_top >= m_max_generation)
@ -864,8 +863,6 @@ namespace euf {
pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data()); pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data());
m_consequences.push_back(r); m_consequences.push_back(r);
TRACE(euf_completion, tout << "new instantiation: " << r << " q: " << mk_pp(q, m) << "\n"); TRACE(euf_completion, tout << "new instantiation: " << r << " q: " << mk_pp(q, m) << "\n");
verbose_stream() << mk_pp(q, m) << " " << r
<< "\n ";
add_constraint(r, pr, d); add_constraint(r, pr, d);
propagate_rules(); propagate_rules();
m_egraph.propagate(); m_egraph.propagate();