From 85c3d874dc3eb4c6097d48d4ad0a53e34ada72f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jul 2022 16:57:41 -0700 Subject: [PATCH] neatify Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_size_reduction_tactic.cpp | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 22c1f0b9e..18083452b 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -115,12 +115,21 @@ public: auto match_bitmask = [&](expr* lhs, expr* rhs) { unsigned lo, hi; expr* arg; - if (m_util.is_numeral(rhs, val, bv_sz) && val.is_zero() && m_util.is_extract(lhs, lo, hi, arg) && lo > 0 && hi + 1 == m_util.get_bv_size(arg) && is_uninterp_const(arg) ) { - val = rational::power_of_two(lo - 1) -1 ; - update_unsigned_upper(to_app(arg), val); - return true; - } - return false; + if (!m_util.is_numeral(rhs, val, bv_sz)) + return false; + if (!val.is_zero()) + return false; + if (!m_util.is_extract(lhs, lo, hi, arg)) + return false; + if (lo == 0) + return false; + if (hi + 1 != m_util.get_bv_size(arg)) + return false; + if (!is_uninterp_const(arg)) + return false; + val = rational::power_of_two(lo - 1) -1 ; + update_unsigned_upper(to_app(arg), val); + return true; }; for (unsigned i = 0; i < sz; i++) {