mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 05:46:08 +00:00
Code Activity

extend cases for process_formulas_on_stack

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-18 12:45:45 -07:00
parent 6c6ea2424b
commit 0438e9a459
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_model_finder.cpp
View file

@ -2288,7 +2288,10 @@ namespace smt {
process_literal(to_app(curr)->get_arg(1), pol); process_literal(to_app(curr)->get_arg(1), pol);
break; break;
case OP_XOR: case OP_XOR:
process_iff(to_app(curr)); for (expr *arg : *to_app(curr)) {
visit_formula(arg, pol);
visit_formula(arg, neg(pol));
}
break; break;
case OP_OR: case OP_OR:
case OP_AND: case OP_AND: