mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-02 03:36:53 +00:00
Code Activity

Merge pull request #8805 from Z3Prover/qmbi_crash

Browse source 
Fix assertion violation in q_mbi diagnostic output
This commit is contained in:
Lev Nachmanson 2026-02-28 11:28:51 -10:00 • committed by GitHub
commit 38ab05e50a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/q_mbi.cpp
View file

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