Skip to content

Commit 497f06f

Browse files
committed
correctly convert object_address
1 parent 1a48120 commit 497f06f

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
@@ -419,6 +419,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
419419
CHECK_RETURN(bv_opt->size() == bits);
420420
return *bv_opt;
421421
}
422+
else if(expr.id() == ID_object_address)
423+
{
424+
const auto &object_address_expr = to_object_address_expr(expr);
425+
return add_addr(object_address_expr.object_expr());
426+
}
422427
else if(expr.id()==ID_constant)
423428
{
424429
const constant_exprt &c = to_constant_expr(expr);
@@ -756,11 +761,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
756761

757762
return bv_utils.zero_extension(op0, width);
758763
}
759-
else if(expr.id() == ID_object_address)
760-
{
761-
const auto &object_address_expr = to_object_address_expr(expr);
762-
return add_addr(object_address_expr.object_expr());
763-
}
764764

765765
return SUB::convert_bitvector(expr);
766766
}

0 commit comments

Comments
 (0)