diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 4ca4928d0..f3a3e9238 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -503,7 +503,7 @@ namespace smt { tout << "lower: " << lower << "\n"; tout << "upper: " << upper << "\n";); - mk_axiom(eqz, eq, true); + mk_axiom(eqz, eq, false); mk_axiom(eqz, lower, false); mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor)); rational k;