From 0438e9a4595d2448dfe0c0aba89ea72d2ee78991 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Jun 2026 12:45:45 -0700 Subject: [PATCH] extend cases for process_formulas_on_stack Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 54a763ac6..3f6c5046e 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2288,7 +2288,10 @@ namespace smt { process_literal(to_app(curr)->get_arg(1), pol); break; case OP_XOR: - process_iff(to_app(curr)); + for (expr *arg : *to_app(curr)) { + visit_formula(arg, pol); + visit_formula(arg, neg(pol)); + } break; case OP_OR: case OP_AND: