Skip to content

Commit 84f150b

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
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 f00593b commit 84f150b

File tree

1 file changed

+8
-6
lines changed

1 file changed

+8
-6
lines changed

src/solvers/flattening/boolbv_get.cpp

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -120,15 +120,17 @@ exprt boolbvt::bv_get_rec(
120120
}
121121
else if(type.id()==ID_struct_tag)
122122
{
123-
return
124-
bv_get_rec(
125-
bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
123+
exprt result = bv_get_rec(
124+
bv, unknown, offset, ns.follow_tag(to_struct_tag_type(type)));
125+
result.type() = type;
126+
return result;
126127
}
127128
else if(type.id()==ID_union_tag)
128129
{
129-
return
130-
bv_get_rec(
131-
bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
130+
exprt result =
131+
bv_get_rec(bv, unknown, offset, ns.follow_tag(to_union_tag_type(type)));
132+
result.type() = type;
133+
return result;
132134
}
133135
else if(type.id()==ID_struct)
134136
{

0 commit comments

Comments
 (0)