From a2b18a37ec2a8c2a031956ae8b4bddf4340719e8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 31 Jul 2019 06:55:10 +0800
Subject: [PATCH] fix #2449
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/rewriter/arith_rewriter.cpp | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index b2d9fcb5d..c6e8b9d62 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -467,15 +467,15 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
case LE:
result = m().mk_or(
m().mk_and(is_zero, m_util.mk_le(div0, arg2)),
- m().mk_and(m_util.mk_gt(e2, zero), m_util.mk_le(e1, mul2)),
- m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_ge(e1, mul2)));
- return BR_REWRITE2;
+ m().mk_and(m().mk_not(m_util.mk_le(e2, zero)), m_util.mk_le(e1, mul2)),
+ m().mk_and(m().mk_not(m_util.mk_ge(e2, zero)), m_util.mk_ge(e1, mul2)));
+ return BR_REWRITE_FULL;
case GE:
result = m().mk_or(
m().mk_and(is_zero, m_util.mk_ge(div0, arg2)),
- m().mk_and(m_util.mk_gt(e2, zero), m_util.mk_ge(e1, mul2)),
- m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_le(e1, mul2)));
- return BR_REWRITE2;
+ m().mk_and(m().mk_not(m_util.mk_le(e2, zero)), m_util.mk_ge(e1, mul2)),
+ m().mk_and(m().mk_not(m_util.mk_ge(e2, zero)), m_util.mk_le(e1, mul2)));
+ 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;