From 4388719848f94cd6bf7025ac308d83c22b658169 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 14 Oct 2022 18:56:18 +0200
Subject: [PATCH] adjust logging

---
 src/sat/sat_drat.cpp              | 1 -
 src/sat/smt/arith_diagnostics.cpp | 2 +-
 src/sat/smt/arith_solver.cpp      | 1 -
 3 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 17de0fe3b..647f8681c 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -656,7 +656,6 @@ namespace sat {
         if (m_out) dump(1, &l, st);
         if (m_bout) bdump(1, &l, st);
         if (m_check) append(l, st);
-        TRACE("sat", tout << "add " << m_clause_eh << "\n");
         if (m_clause_eh) m_clause_eh->on_clause(1, &l, st);
     }
     void drat::add(literal l1, literal l2, status st) {
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index f74adf38b..2be19182a 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -69,7 +69,7 @@ namespace arith {
     }
 
     std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { 
-        return euf::th_explain::from_index(idx).display(out);
+        return euf::th_explain::from_index(idx).display(out << "arith ");
     }
 
     std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { 
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 685d9249a..f7e3f6293 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -76,7 +76,6 @@ namespace arith {
     }
 
     bool solver::unit_propagate() {
-        TRACE("arith", tout << "unit propagate\n";);
         m_model_is_initialized = false;
         if (!m_solver->has_changed_columns() && !m_new_eq && m_new_bounds.empty() && m_asserted_qhead == m_asserted.size())
             return false;