Skip to content

Commit caab966

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 e7d87ae commit caab966

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

48704870
if(recstack.find(id) == recstack.end())
48714871
{
4872+
const auto &base_struct = ns.follow_tag(struct_tag);
48724873
recstack.insert(id);
4873-
find_symbols_rec(ns.follow_tag(struct_tag), recstack);
4874+
find_symbols_rec(base_struct, recstack);
4875+
datatype_map[type] = datatype_map[base_struct];
48744876
}
48754877
}
48764878
else if(type.id() == ID_union_tag)

0 commit comments

Comments
 (0)