updated logging

Z3Prover · Oct 7, 2020 · ae7d767 · ae7d767
1 parent 546e152
commit ae7d767
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 10 deletions.
diff --git 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
@@ -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";
                   );