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: