From a595e987073bb8e329ef5bd016022d93ab37be2a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 May 2026 18:57:21 -0700 Subject: [PATCH] fix regression: m_tmp_diseq has 0 arguments, you have to access the expression Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f4dce7f8b..d55b2d98d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1137,7 +1137,7 @@ namespace smt { m.inc_ref(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()); app * eq = m.mk_eq(n1->get_expr(), n2->get_expr()); m.inc_ref(eq);