mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove verbose output

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-16 13:23:56 -08:00
parent 50f9fddfd2
commit fe27ca1dd0
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/qe/mbp/mbp_euf.cpp
View file

@ -128,8 +128,6 @@ namespace mbp {
m_parents.insert_if_not_there(arg, {}).push_back(t); m_parents.insert_if_not_there(arg, {}).push_back(t);
} }
} }
for (auto [key, value] : m_reps)
verbose_stream() << mk_pp(key, m) << " -> " << mk_pp(value, m) << "\n";
unsigned j = 0; unsigned j = 0;
bool solved = false; bool solved = false;
for (app* v : vars) { for (app* v : vars) {
@ -204,7 +202,6 @@ namespace mbp {
for (auto e : partition) { for (auto e : partition) {
if (a == e) if (a == e)
continue; continue;
verbose_stream() << "Unify " << mk_pp(a, m) << " with " << mk_pp(e, m) << "\n";
if (!same_decl(a, e)) if (!same_decl(a, e))
continue; continue;
app* b = to_app(e); app* b = to_app(e);