From 6c6ea2424b9cab20da0a26ad79a993cc15e19ab3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Jun 2026 12:39:39 -0700 Subject: [PATCH] extend cases for process_formulas_on_stack Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 94c9fa0ba..54a763ac6 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2283,9 +2283,12 @@ namespace smt { if (is_app(curr)) { if (to_app(curr)->get_family_id() == m.get_basic_family_id() && m.is_bool(curr)) { switch (static_cast(to_app(curr)->get_decl_kind())) { - case OP_IMPLIES: + case OP_IMPLIES: + process_literal(to_app(curr)->get_arg(0), neg(pol)); + process_literal(to_app(curr)->get_arg(1), pol); + break; case OP_XOR: - UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs + process_iff(to_app(curr)); break; case OP_OR: case OP_AND: