From 441dbbb94bc7bd71f56d440b0029b473a3918e21 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Nov 2016 13:08:50 -0800
Subject: [PATCH] streamline logging in arithmetic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_aux.h  | 4 ++--
 src/smt/theory_arith_core.h | 8 +++++---
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 50bfee20e..de357c8d3 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -417,8 +417,8 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::atom::display(theory_arith<Ext> const& th, std::ostream& out) const {
         literal l(get_bool_var(), !m_is_true);
-        out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
-        out << l << ":";
+        // out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
+        // out << l << ":";
         th.get_context().display_detailed_literal(out, l);
     }
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 07d30222b..a08ee50ab 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1069,7 +1069,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::flush_bound_axioms() {
-        CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
+        CTRACE("arith_verbose", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
 
         while (!m_new_atoms.empty()) {
             ptr_vector<atom> atoms;            
@@ -1084,7 +1084,7 @@ namespace smt {
                     --i;
                 }
             }            
-            CTRACE("arith", !atoms.empty(),  
+            CTRACE("arith", atoms.size() > 1,  
                   for (unsigned i = 0; i < atoms.size(); ++i) {
                       atoms[i]->display(*this, tout); tout << "\n";
                   });
@@ -1292,7 +1292,7 @@ namespace smt {
     
     template<typename Ext>
     void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
-        TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
+        TRACE("arith_verbose", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
         atom * a = get_bv2a(v);
         if (!a) return;
         SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@@ -3043,12 +3043,14 @@ namespace smt {
         m_stats.m_conflicts++;
         m_num_conflicts++;
         TRACE("arith_conflict", 
+              tout << "scope: " << ctx.get_scope_level() << "\n";
               for (unsigned i = 0; i < num_literals; i++) {
                   ctx.display_detailed_literal(tout, lits[i]);
                   tout << " ";
                   if (coeffs_enabled()) {
                       tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
                   }
+                  tout << "\n";
               }
               for (unsigned i = 0; i < num_eqs; i++) {
                   tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";