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);