mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
parent
2a1f05e7e8
commit
3dcfbb8347
|
@ -478,7 +478,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
|
|||
return BR_REWRITE_FULL;
|
||||
case EQ:
|
||||
result = m().mk_ite(is_zero, m().mk_eq(div0, arg2), m().mk_eq(e1, mul2));
|
||||
return BR_REWRITE2;
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
|
||||
|
|
|
@ -811,15 +811,13 @@ namespace smt {
|
|||
bool theory_arith<Ext>::is_monomial_linear(expr * m) const {
|
||||
SASSERT(is_pure_monomial(m));
|
||||
unsigned num_nl_vars = 0;
|
||||
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
|
||||
expr * arg = to_app(m)->get_arg(i);
|
||||
for (expr* arg : *to_app(m)) {
|
||||
theory_var _var = expr2var(arg);
|
||||
if (!is_fixed(_var)) {
|
||||
num_nl_vars++;
|
||||
}
|
||||
else {
|
||||
if (lower_bound(_var).is_zero())
|
||||
return true;
|
||||
else if (lower_bound(_var).is_zero()) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return num_nl_vars <= 1;
|
||||
|
|
Loading…
Reference in a new issue