From e6d527c5d576333ce8be7d9ace47aa52603956aa Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 2 May 2017 15:39:15 -0400
Subject: [PATCH] remove trace code from theory_arith

---
 src/smt/theory_arith.h      | 14 +------------
 src/smt/theory_arith_core.h | 41 ++-----------------------------------
 2 files changed, 3 insertions(+), 52 deletions(-)

diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index eb36a92fb..439adbdff 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -577,19 +577,7 @@ namespace smt {
             return is_free(get_context().get_enode(n)->get_th_var(get_id())); 
         }
         bool is_fixed(theory_var v) const;
-        void set_bound_core(theory_var v, bound * new_bound, bool upper) {
-            TRACE("t_str_int",
-                    tout << "setting " << (upper ? "upper" : "lower") << " bound ";
-                    if (new_bound) {
-                        tout << new_bound->get_value();
-                    } else {
-                        tout << "(NULL)";
-                    }
-                    tout << " for theory var v#" << v;
-                    tout << std::endl;
-            );
-            m_bounds[static_cast<unsigned>(upper)][v] = new_bound;
-        }
+        void set_bound_core(theory_var v, bound * new_bound, bool upper) { m_bounds[static_cast<unsigned>(upper)][v] = new_bound; }
         void restore_bound(theory_var v, bound * new_bound, bool upper) { set_bound_core(v, new_bound, upper); }
         void restore_nl_propagated_flag(unsigned old_trail_size);
         void set_bound(bound * new_bound, bool upper);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 7fed094da..dd1924e44 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3263,50 +3263,13 @@ namespace smt {
     bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
         theory_var v = n->get_th_var(get_id());
         inf_numeral val;
-        // rewrites for tracing purposes
-        if (v == null_theory_var) {
-            TRACE("t_str_int", tout << "WARNING: enode " << mk_pp(n->get_owner(), get_manager())
-                    << " attached to null theory var" << std::endl;
-            );
-            return false;
-        } else {
-            val = get_value(v);
-            TRACE("t_str_int", tout << "enode " << mk_pp(n->get_owner(), get_manager())
-                    << " attached to theory var v#" << v
-                    << ", has val = " << val
-                    << std::endl;
-                    );
-            if (!is_int(v) || val.is_int()) {
-                return to_expr(val, is_int(v), r);
-            } else {
-                return false;
-            }
-        }
-        // return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
+        return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
     }
 
     template<typename Ext>
     bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) {        
         theory_var v = n->get_th_var(get_id());
-        bound * b;
-        if (v == null_theory_var) {
-            TRACE("t_str_int", tout << "WARNING: enode " << mk_pp(n->get_owner(), get_manager())
-                    << " attached to null theory var" << std::endl;
-            );
-            b = 0;
-        } else {
-            b = lower(v);
-            TRACE("t_str_int",
-                    tout << "enode " << mk_pp(n->get_owner(), get_manager())
-                    << " attached to theory var v#" << v
-                    << std::endl;
-                    if (b) {
-                        tout << "lower bound = " << b->get_value() << std::endl;
-                    } else {
-                        tout << "WARNING: b = NULL" << std::endl;
-                    }
-                    );
-        }
+        bound * b = (v == null_theory_var) ? 0 : lower(v);
         return b && to_expr(b->get_value(), is_int(v), r);
     }