Skip to content

Commit 3e74881

Browse files
SaswatPadhithomasspriggs
authored andcommitted
Fix SMT2 DT encoding of structs
This commit fixes a `key not found` exception in `convert_type` during SMT2 encoding of structs using data types. Although structs were being mapped to SMT2 datatypes (in `datatype_map`) struct_tags were not.
1 parent 7dc7632 commit 3e74881

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4890,8 +4890,10 @@ void smt2_convt::find_symbols_rec(
48904890

48914891
if(recstack.find(id) == recstack.end())
48924892
{
4893+
const auto &base_struct = ns.follow_tag(struct_tag);
48934894
recstack.insert(id);
4894-
find_symbols_rec(ns.follow_tag(struct_tag), recstack);
4895+
find_symbols_rec(base_struct, recstack);
4896+
datatype_map[type] = datatype_map[base_struct];
48954897
}
48964898
}
48974899
else if(type.id() == ID_union_tag)

0 commit comments

Comments
 (0)