From 2f49094d490e3536b1da93b0fb513144a3b327a5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 26 Jul 2021 19:36:16 -0700
Subject: [PATCH] change debug output

---
 src/qe/mbp/mbp_arith.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 31329b3dd..a2101e2d1 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -47,7 +47,6 @@ namespace mbp {
         ~imp() {}
 
         void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
-            // TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
             rational w;
             if (ts.find(x, w)) 
                 ts.insert(x, w + v);            
@@ -362,6 +361,10 @@ namespace mbp {
                 optdefs2mbpdef(defs, index2expr, real_vars, result);     
             if (m_apply_projection)
                 apply_projection(result, fmls);
+            TRACE("qe",
+                for (auto [v, t] : result)
+                    tout << v << " := " << t << "\n";
+                tout << "fmls:" << fmls << "\n";);
             return result;
         }