Skip to content

Commit 0eb2cb3

Browse files
committed
correctly convert object_address
1 parent 7d96a2a commit 0eb2cb3

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);
@@ -753,11 +758,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
753758

754759
return bv_utils.zero_extension(op0, width);
755760
}
756-
else if(expr.id() == ID_object_address)
757-
{
758-
const auto &object_address_expr = to_object_address_expr(expr);
759-
return add_addr(object_address_expr.object_expr());
760-
}
761761

762762
return SUB::convert_bitvector(expr);
763763
}

0 commit comments

Comments
 (0)