diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index c11c54b69..f96b6228b 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -506,7 +506,7 @@ namespace smt {
 
             mk_axiom(eqz, eq,    true);
             mk_axiom(eqz, lower, false);
-            mk_axiom(eqz, upper, false);
+            mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
             rational k;
             context& ctx = get_context();
             (void)ctx;