From 3b4f976118e3dc4b5dbc369e7d50753abd8caa82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Nov 2021 19:15:03 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/smt/theory_user_propagator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index ce6fa8241..9e10b96c5 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -53,7 +53,7 @@ void theory_user_propagator::propagate_cb( unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) { CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true, - tout << "redundant consequence: " << mk_pp(conseq, m) << "\n"); + ctx.display(tout << "redundant consequence: " << mk_pp(conseq, m) << "\n")); if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) return; m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));