mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #2449

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-31 06:55:10 +08:00
parent e1fd167e01
commit a2b18a37ec
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/arith_rewriter.cpp
View file

@ -467,15 +467,15 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
case LE: case LE:
result = m().mk_or( result = m().mk_or(
m().mk_and(is_zero, m_util.mk_le(div0, arg2)), 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().mk_not(m_util.mk_le(e2, zero)), m_util.mk_le(e1, mul2)),
m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_ge(e1, mul2))); m().mk_and(m().mk_not(m_util.mk_ge(e2, zero)), m_util.mk_ge(e1, mul2)));
return BR_REWRITE2; return BR_REWRITE_FULL;
case GE: case GE:
result = m().mk_or( result = m().mk_or(
m().mk_and(is_zero, m_util.mk_ge(div0, arg2)), 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().mk_not(m_util.mk_le(e2, zero)), m_util.mk_ge(e1, mul2)),
m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_le(e1, mul2))); m().mk_and(m().mk_not(m_util.mk_ge(e2, zero)), m_util.mk_le(e1, mul2)));
return BR_REWRITE2; return BR_REWRITE_FULL;
case EQ: case EQ:
result = m().mk_ite(is_zero, m().mk_eq(div0, arg2), m().mk_eq(e1, mul2)); result = m().mk_ite(is_zero, m().mk_eq(div0, arg2), m().mk_eq(e1, mul2));
return BR_REWRITE2; return BR_REWRITE2;