From 95963f71f43e5d722e8941aff602047f28bc5b9a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 11 Aug 2018 17:18:11 -0700
Subject: [PATCH] fix bug introduced in fix of #1798
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_arith_core.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
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;