From 213d816c0a418bafc8fe57acb4b10aeea5b1f5b2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 24 Nov 2014 18:10:54 +0000 Subject: [PATCH] Bugfix for bv_size_reduction. Thanks to user rsas for reporting this isse! Signed-off-by: Christoph M. Wintersteiger --- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index e149afc75..14a2fb28d 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -229,7 +229,7 @@ struct bv_size_reduction_tactic::imp { else { // l < u if (l.is_neg()) { - unsigned i_nb = (u - l).get_num_bits(); + unsigned i_nb = (u - l).get_num_bits() + 1; unsigned v_nb = m_util.get_bv_size(v); if (i_nb < v_nb) { new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));