From f313ab9e4c4c7fd8e81dfd070b8e70e35de95d47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 May 2020 10:15:06 -0700 Subject: [PATCH] correct newly introduced rewrite --- src/ast/rewriter/bv_rewriter.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 71c043eb6..6a2c4d3cd 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -510,10 +510,14 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref return BR_REWRITE2; } - // (bvule c (+ c a)) -> (bvule a (2^n - c)) (could be generalized) - if (!is_signed && is_num1 && m_util.is_bv_add(b, a1, a2) && is_numeral(a1, r2, sz) && r1 == r2) { - result = m_util.mk_ule(a2, m_util.mk_numeral(-r1, sz)); - return BR_REWRITE1; + // (bvule r1 (+ r2 a)) -> + // for r1 = r2, (bvule a (2^n - r2 - 1)) + // other cases r1 > r2, r1 < r2 are TBD + if (!is_signed && is_num1 && m_util.is_bv_add(b, a1, a2) && is_numeral(a1, r2, sz)) { + if (r1 == r2) { + result = m_util.mk_ule(a2, m_util.mk_numeral(-r2 - 1, sz)); + return BR_REWRITE1; + } } if (m_le_extra) {