mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 15:40:37 +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:39:39 -07:00
parent 72973b00eb
commit 6c6ea2424b
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_model_finder.cpp
View file

@ -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<basic_op_kind>(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: