From 93ac330864a599de3adf5e6bdb18edf2415d7598 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 28 Feb 2026 11:15:28 -1000 Subject: [PATCH] Fix assertion violation in q_mbi diagnostic output The IF_VERBOSE(0,...) block at line 498 in q_mbi.cpp used operator[] on values2root map which asserts the key exists. When the model evaluation of the inverted term produces a value not present in the EUF values2root map, this crashes. Use find() instead to handle the missing key gracefully, since this is diagnostic output and the missing key is expected when the model inversion produces inconsistent results. Fixes assertion violation from #7027 (obj_hashtable.h line 168/174) with forall/array/eq2ineq combination. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/sat/smt/q_mbi.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 41d5b867a..f390351df 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -499,8 +499,12 @@ namespace q { IF_VERBOSE(0, verbose_stream() << mk_pp(s, m) << " := " << (*m_model)(s) << "\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"; + euf::enode* nr = nullptr; + auto const& v2r = ctx.values2root(); + if (v2r.find((*m_model)(term), nr)) + verbose_stream() << value << " -> " << (*m_model)(nr->get_expr()) << "\n"; + if (v2r.find((*m_model)(s), nr)) + verbose_stream() << (*m_model)(s) << " -> " << (*m_model)(nr->get_expr()) << "\n"; verbose_stream() << *m_model << "\n";); } eqs.push_back(eq);