From 196788a0915d69b8599bd7a89dd4d644f324a537 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Nov 2022 12:09:56 -0800 Subject: [PATCH] bug fix for equality solving --- src/ast/simplifiers/elim_unconstrained.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 2cdca3074a9..94201dde7b6 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -81,9 +81,9 @@ void elim_unconstrained::eliminate() { m_args.reset(); for (expr* arg : *to_app(t)) m_args.push_back(get_node(arg).m_term); - if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) + if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) continue; - + SASSERT(r->get_sort() == t->get_sort()); m_stats.m_num_eliminated++; n.m_refcount = 0; SASSERT(r);