From ae7d76767b614dd8f77a692e00d6d157df31e03d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Oct 2020 18:02:20 -0700
Subject: [PATCH] updated logging

---
 src/smt/fingerprints.cpp   | 10 +++-------
 src/smt/smt_quantifier.cpp |  6 +++---
 2 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/smt/fingerprints.cpp b/src/smt/fingerprints.cpp
index b9d4571da05..490f62aa513 100644
--- a/src/smt/fingerprints.cpp
+++ b/src/smt/fingerprints.cpp
@@ -66,18 +66,13 @@ namespace smt {
         fingerprint * d = mk_dummy(data, data_hash, num_args, args);
         if (m_set.contains(d)) 
             return nullptr;
-        TRACE("fingerprint_bug", tout << "1) inserting: " << data_hash << " num_args: " << num_args;
-              for (unsigned i = 0; i < num_args; i++) tout << " " << args[i]->get_owner_id(); 
-              tout << "\n";);
         for (unsigned i = 0; i < num_args; i++)
             d->m_args[i] = d->m_args[i]->get_root();
         if (m_set.contains(d)) {
-            TRACE("fingerprint_bug", tout << "failed: " << data_hash << " num_args: " << num_args;
-                  for (unsigned i = 0; i < num_args; i++) tout << " " << d->m_args[i]->get_owner_id(); 
-                  tout << "\n";);
+            TRACE("fingerprint_bug", tout << "failed: " << *d;);
             return nullptr;
         }
-        TRACE("fingerprint_bug", tout << "2) inserting: " << *d;);
+        TRACE("fingerprint_bug", tout << "inserting @" << m_scopes.size() << " " << *d;);
         fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, def, num_args, d->m_args);
         m_fingerprints.push_back(f);
         m_defs.push_back(def);
@@ -117,6 +112,7 @@ namespace smt {
         m_fingerprints.shrink(old_size);
         m_defs.shrink(old_size);
         m_scopes.shrink(new_lvl);
+        TRACE("fingerprint_bug", tout << "pop @" << m_scopes.size() << "\n";);
     }
 
     void fingerprint_set::display(std::ostream & out) const {
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 72219e7fd18..8de933c447a 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -313,10 +313,10 @@ namespace smt {
                 m_num_instances++;
             }
 
-            CTRACE("quantifier_", f != nullptr, 
-                  tout << expr_ref(q, m()) << " ";
+            CTRACE("bindings", f != nullptr, 
+                  tout << expr_ref(q, m()) << "\n";
                   for (unsigned i = 0; i < num_bindings; ++i) {
-                      tout << expr_ref(bindings[i]->get_owner(), m()) << " ";
+                      tout << expr_ref(bindings[i]->get_owner(), m()) << " [r " << bindings[i]->get_root()->get_owner_id() << "] ";
                   }
                   tout << "\n";
                   );