From 99e2794a6db5aba5db6fd5eea55462e403eb886d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Nov 2023 17:20:39 -0800 Subject: [PATCH] update output Signed-off-by: Nikolaj Bjorner --- src/sat/smt/q_mbi.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index c66f1b3a2..539c4f943 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -498,8 +498,8 @@ namespace q { if (m_model->is_false(eq)) { IF_VERBOSE(0, verbose_stream() << mk_pp(s, m) << " := " << (*m_model)(s) << "\n"; - verbose_stream() << mk_pp(term, m) << " := " << (*m_model)(term) << "\n"; - verbose_stream() << value << " -> " << (*m_model)(ctx.values2root()[value]->get_expr()) << "\n"; + verbose_stream() << term << " := " << (*m_model)(term) << "\n"; + verbose_stream() << value << " -> " << (*m_model)(ctx.values2root()[(*m_model)(term)]->get_expr()) << "\n"; verbose_stream() << (*m_model)(s) << " -> " << (*m_model)(ctx.values2root()[(*m_model)(s)]->get_expr()) << "\n"; verbose_stream() << *m_model << "\n";); }