From 2050fc3b358ea96a9bdd9a8775a3c51ed8d67885 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Mon, 27 Jan 2025 22:09:48 +0100 Subject: [PATCH] Preserve fingerprint in trace (#7534) --- src/smt/qi_queue.cpp | 2 +- src/smt/smt_quantifier.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index ff602ba92..006ee398a 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -188,7 +188,7 @@ namespace smt { void qi_queue::display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation) { if (m.has_trace_stream()) { - m.trace_stream() << "[instance] 0x0"; + m.trace_stream() << "[instance] " << f->get_data_hash(); if (m.proofs_enabled()) m.trace_stream() << " #" << proof_id; m.trace_stream() << " ; " << generation; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index a8863414c..f605e3b57 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -240,7 +240,7 @@ namespace smt { vector> & used_enodes) { if (pat == nullptr) { - trace_stream() << "[inst-discovered] MBQI 0x0 #" << q->get_id(); + trace_stream() << "[inst-discovered] MBQI " << f->get_data_hash() << " #" << q->get_id(); for (unsigned i = 0; i < num_bindings; ++i) { trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id(); } @@ -266,7 +266,7 @@ namespace smt { } // At this point all relevant equalities for the match are logged. - out << "[new-match] " << static_cast(f) << " #" << q->get_id() << " #" << pat->get_id(); + out << "[new-match] " << f->get_data_hash() << " #" << q->get_id() << " #" << pat->get_id(); for (unsigned i = 0; i < num_bindings; i++) { // I don't want to use mk_pp because it creates expressions for pretty printing. // This nasty side-effect may change the behavior of Z3.