From 016732aa5936452bf133adc3281da2a9d77cc200 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Oct 2019 17:21:39 -0700
Subject: [PATCH] move some tracing to verbose

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_solver.cpp  | 8 ++++----
 src/smt/theory_datatype.cpp | 1 +
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 4e26a72c0..41c60c80d 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -562,8 +562,8 @@ namespace nlsat {
 
         void del(atom * a) {
             if (a == nullptr)
-                return ;
-            TRACE("nlsat", display(tout << "del: b" << a->m_bool_var << " ", *a) << "\n";);
+                return;
+            TRACE("nlsat_verbose", display(tout << "del: b" << a->m_bool_var << " ", *a) << "\n";);
             if (a->is_ineq_atom())
                 del(to_ineq_atom(a));
             else
@@ -625,7 +625,7 @@ namespace nlsat {
                 bool_var b = mk_bool_var_core();
                 m_atoms[b] = atom;
                 atom->m_bool_var = b;
-                TRACE("nlsat", display(tout << "create: b" << atom->m_bool_var << " ", *atom) << "\n";);
+                TRACE("nlsat_verbose", display(tout << "create: b" << atom->m_bool_var << " ", *atom) << "\n";);
                 return b;
             }
         }
@@ -1733,7 +1733,7 @@ namespace nlsat {
                   tout << "new valid clause:\n";
                   display(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr()) << "\n";);
 
-            if (m_check_lemmas) {
+            if (m_check_lemmas && false) {
                 check_lemma(m_lazy_clause.size(), m_lazy_clause.c_ptr(), true, nullptr);
             }
 
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 6af48b823..d8266f2bb 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -945,6 +945,7 @@ namespace smt {
         func_decl * r         = nullptr;
         m_stats.m_splits++;
 
+
         if (d->m_recognizers.empty()) {
             r = m_util.get_constructor_is(non_rec_c);
         }