mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
parent
99f20c59e4
commit
2da7a8dd70
|
@ -345,7 +345,7 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp
|
|||
continue;
|
||||
eqs.push_back(m().mk_eq(arg, zero));
|
||||
}
|
||||
result = m().mk_and(eqs);
|
||||
result = m().mk_or(eqs);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue