mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix big-int bug for shift amounts, github issue 44, reported by Dejan

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-20 10:20:06 +02:00
parent 7d88d04514
commit 6c1a5390ef
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -902,6 +902,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::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<unsigned>(k.get_int64());
if (n >= sz) n = sz;
unsigned pos;
@ -947,6 +948,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::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<unsigned>(k.get_int64());
unsigned pos = 0;
for (unsigned i = n; i < sz; pos++, i++)
@ -989,6 +991,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::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<unsigned>(k.get_int64());
unsigned pos = 0;
for (unsigned i = n; i < sz; pos++, i++)