File tree 2 files changed +8
-6
lines changed
2 files changed +8
-6
lines changed Original file line number Diff line number Diff line change @@ -253,13 +253,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
253
253
254
254
if (op_type.id ()==ID_pointer)
255
255
return convert_bv (op);
256
- else if (op_type.id ()==ID_signedbv ||
257
- op_type.id ()==ID_unsignedbv ||
258
- op_type.id ()==ID_bool ||
259
- op_type.id ()==ID_c_enum ||
260
- op_type.id ()==ID_c_enum_tag)
256
+ else if (
257
+ can_cast_type<bitvector_typet>(op_type) || op_type.id () == ID_c_enum ||
258
+ op_type.id () == ID_c_enum_tag)
261
259
{
262
- // Cast from integer to pointer.
260
+ // Cast from a bitvector type to pointer.
263
261
// We just do a zero extension.
264
262
265
263
const bvt &op_bv=convert_bv (op);
Original file line number Diff line number Diff line change @@ -741,6 +741,10 @@ std::string smt2_convt::type2id(const typet &type) const
741
741
{
742
742
return type2id (ns.follow_tag (to_c_enum_tag_type (type)).subtype ());
743
743
}
744
+ else if (type.id () == ID_pointer)
745
+ {
746
+ return " p" + std::to_string (to_pointer_type (type).get_width ());
747
+ }
744
748
else
745
749
{
746
750
UNREACHABLE;
You can’t perform that action at this time.
0 commit comments