From fe27ca1dd03feba3d3fe98870a47d09083d531cf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Feb 2025 13:23:56 -0800
Subject: [PATCH] remove verbose output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/mbp/mbp_euf.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/qe/mbp/mbp_euf.cpp b/src/qe/mbp/mbp_euf.cpp
index 850a72812..9c54e11f6 100644
--- a/src/qe/mbp/mbp_euf.cpp
+++ b/src/qe/mbp/mbp_euf.cpp
@@ -128,8 +128,6 @@ namespace mbp {
                     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;
         bool solved = false;
         for (app* v : vars) {
@@ -204,7 +202,6 @@ namespace mbp {
         for (auto e : partition) {
             if (a == e)
                 continue;
-            verbose_stream() << "Unify " << mk_pp(a, m) << " with " << mk_pp(e, m) << "\n";
             if (!same_decl(a, e))
                 continue;
             app* b = to_app(e);