From a0d4a8c21c12a5ee6e8e0c338d9a1389683d8f47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Aug 2022 00:12:44 -0700 Subject: [PATCH] update diagnostics --- src/smt/qi_queue.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index de52cdb0101..f8fbe739eef 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -23,6 +23,7 @@ Revision History: #include "ast/rewriter/var_subst.h" #include "smt/smt_context.h" #include "smt/qi_queue.h" +#include namespace smt { @@ -228,15 +229,12 @@ namespace smt { TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m) << "\n";); - TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m) << "\n";); expr_ref s_instance(m); proof_ref pr(m); m_context.get_rewriter()(instance, s_instance, pr); TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";); if (m.is_true(s_instance)) { - TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m);); - STRACE("instance", tout << "Instance reduced to true\n";); stat -> inc_num_instances_simplify_true(); if (m.has_trace_stream()) { @@ -250,9 +248,11 @@ namespace smt { std::cout << "instantiate\n"; enode_vector _bindings(num_bindings, bindings); for (auto * b : _bindings) - std::cout << enode_pp(b, m_context) << " "; + std::cout << mk_pp(b->get_expr(), m) << " "; std::cout << "\n"; std::cout << mk_pp(q, m) << "\n"; + std::cout << "instance\n"; + std::cout << instance << "\n"; #endif TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);