Skip to content

Commit 57582b3

Browse files
committed
lower_popcount is now independent of bitvector representation
1 parent c6baef2 commit 57582b3

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/solvers/lowering/popcount.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,8 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
4747
bitstring.reserve(new_width);
4848
for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
4949
bitstring += std::string(shift, '0') + std::string(shift, '1');
50-
constant_exprt bitmask(bitstring, x.type());
50+
const mp_integer value = binary2integer(bitstring, false);
51+
constant_exprt bitmask(integer2bv(value, new_width), x.type());
5152
// build the expression
5253
x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
5354
}

0 commit comments

Comments
 (0)