From d9385e9713c2c09739ff1a200480b1c70eb81257 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 a988b1ba4..8dd85f0b9 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2207,7 +2207,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: