From ea181fe8b25928006c2f9af8904899f71ee40165 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Mar 2021 15:01:32 -0800 Subject: [PATCH] more useful trace --- src/smt/smt_context.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ea5655fa2..3a7ecab71 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -464,7 +464,6 @@ namespace smt { enode * r1 = n1->get_root(); enode * r2 = n2->get_root(); - if (r1 == r2) { TRACE("add_eq", tout << "redundant constraint.\n";); return; @@ -755,7 +754,8 @@ namespace smt { enode * r2 = n2->get_root(); enode * r1 = n1->get_root(); if (!r1->has_th_vars() && !r2->has_th_vars()) { - TRACE("merge_theory_vars", tout << "Neither have theory vars #" << n1->get_expr()->get_id() << " #" << n2->get_expr()->get_id() << "\n";); + TRACE("merge_theory_vars", tout << "Neither have theory vars #" + << mk_bounded_pp(n1->get_expr(), m) << " #" << mk_bounded_pp(n2->get_expr(), m) << "\n";); return; }