Skip to content

Commit 4418acb

Browse files
committed
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 ac11ec8 commit 4418acb

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
@@ -4872,8 +4872,10 @@ void smt2_convt::find_symbols_rec(
48724872

48734873
if(recstack.find(id) == recstack.end())
48744874
{
4875+
const auto &base_struct = ns.follow_tag(struct_tag);
48754876
recstack.insert(id);
4876-
find_symbols_rec(ns.follow_tag(struct_tag), recstack);
4877+
find_symbols_rec(base_struct, recstack);
4878+
datatype_map[type] = datatype_map[base_struct];
48774879
}
48784880
}
48794881
else if(type.id() == ID_union_tag)

0 commit comments

Comments
 (0)