Skip to content

Commit 853cefc

Browse files
committed
Simplify typecast over ID_bv and pointers
This has the same semantics as ID_signedbv or ID_unsignedbv.
1 parent d212c21 commit 853cefc

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/util/simplify_expr.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -779,7 +779,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
779779
// (void*)(intX)expr -> (void*)expr
780780
if(
781781
expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
782-
(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv) &&
782+
(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv ||
783+
op_type.id() == ID_bv) &&
783784
to_bitvector_type(op_type).get_width() >=
784785
to_bitvector_type(expr_type).get_width())
785786
{
@@ -1305,7 +1306,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
13051306
// where T1 has fewer bits than T2
13061307
if(
13071308
op_type_id == expr_type_id &&
1308-
(expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1309+
(expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1310+
expr_type_id == ID_bv) &&
13091311
to_bitvector_type(expr_type).get_width() <=
13101312
to_bitvector_type(operand.type()).get_width())
13111313
{

0 commit comments

Comments
 (0)