Skip to content

Commit c25f6fb

Browse files
committed
correctly convert object_address
1 parent 9f7def6 commit c25f6fb

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -416,6 +416,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
416416
CHECK_RETURN(bv_opt->size() == bits);
417417
return *bv_opt;
418418
}
419+
else if(expr.id() == ID_object_address)
420+
{
421+
const auto &object_address_expr = to_object_address_expr(expr);
422+
return add_addr(object_address_expr.object_expr());
423+
}
419424
else if(expr.id()==ID_constant)
420425
{
421426
const constant_exprt &c = to_constant_expr(expr);
@@ -750,11 +755,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
750755

751756
return bv_utils.zero_extension(op0, width);
752757
}
753-
else if(expr.id() == ID_object_address)
754-
{
755-
const auto &object_address_expr = to_object_address_expr(expr);
756-
return add_addr(object_address_expr.object_expr());
757-
}
758758

759759
return SUB::convert_bitvector(expr);
760760
}

0 commit comments

Comments
 (0)