Skip to content

Commit 5cd5f12

Browse files
committed
Make sure boolbv::get returns tag types when requested
boolbv::get should return expressions of exactly the same type, not an expanded version of the type.
1 parent b614c03 commit 5cd5f12

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

src/solvers/flattening/boolbv_get.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -120,15 +120,19 @@ exprt boolbvt::bv_get_rec(
120120
}
121121
else if(type.id()==ID_struct_tag)
122122
{
123-
return
123+
exprt result=
124124
bv_get_rec(
125125
bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
126+
result.type() = type;
127+
return std::move(result);
126128
}
127129
else if(type.id()==ID_union_tag)
128130
{
129-
return
131+
exprt result=
130132
bv_get_rec(
131133
bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
134+
result.type() = type;
135+
return std::move(result);
132136
}
133137
else if(type.id()==ID_struct)
134138
{

0 commit comments

Comments
 (0)