mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

fix regression: m_tmp_diseq has 0 arguments, you have to access the expression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-30 18:57:21 -07:00
parent dbe986fdf7
commit a595e98707
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -1137,7 +1137,7 @@ namespace smt {
m.inc_ref(eq); m.inc_ref(eq);
_this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq); _this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq);
} }
else if (m_is_diseq_tmp->get_arg(0)->get_sort() != n1->get_sort()) { else if (m_is_diseq_tmp->get_app()->get_arg(0)->get_sort() != n1->get_sort()) {
m.dec_ref(m_is_diseq_tmp->get_expr()); m.dec_ref(m_is_diseq_tmp->get_expr());
app * eq = m.mk_eq(n1->get_expr(), n2->get_expr()); app * eq = m.mk_eq(n1->get_expr(), n2->get_expr());
m.inc_ref(eq); m.inc_ref(eq);