From 6c1a5390ef202499d86fdb41415dada7db1c9d76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Apr 2015 10:20:06 +0200 Subject: [PATCH] fix big-int bug for shift amounts, github issue 44, reported by Dejan Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index b579d698eba..a30c0d32c37 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -902,6 +902,7 @@ template void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { numeral k; if (is_numeral(sz, b_bits, k)) { + if (k > numeral(sz)) k = numeral(sz); unsigned n = static_cast(k.get_int64()); if (n >= sz) n = sz; unsigned pos; @@ -947,6 +948,7 @@ template void bit_blaster_tpl::mk_lshr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { numeral k; if (is_numeral(sz, b_bits, k)) { + if (k > numeral(sz)) k = numeral(sz); unsigned n = static_cast(k.get_int64()); unsigned pos = 0; for (unsigned i = n; i < sz; pos++, i++) @@ -989,6 +991,7 @@ template void bit_blaster_tpl::mk_ashr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { numeral k; if (is_numeral(sz, b_bits, k)) { + if (k > numeral(sz)) k = numeral(sz); unsigned n = static_cast(k.get_int64()); unsigned pos = 0; for (unsigned i = n; i < sz; pos++, i++)