Merge pull request #5904 from padhi-aws-forks/smt_struct_fix

Fix a crash during SMT translation of structs

Author: SaswatPadhi

regression/cbmc/struct15/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+struct test
+{
+  unsigned int a;
+  unsigned int b;
+};
+
+int main()
+{
+  struct test t;
+  if(t.a > 10)
+    assert(t.a > 0);
+}

regression/cbmc/struct15/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--trace --z3
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^map::at:
+key not found
+--
+This test checks the encoding of C `struct`s using SMT2 data types.

src/solvers/smt2/smt2_conv.cpp

@@ -4890,8 +4890,10 @@ void smt2_convt::find_symbols_rec(
 
     if(recstack.find(id) == recstack.end())
     {
+      const auto &base_struct = ns.follow_tag(struct_tag);
       recstack.insert(id);
-      find_symbols_rec(ns.follow_tag(struct_tag), recstack);
+      find_symbols_rec(base_struct, recstack);
+      datatype_map[type] = datatype_map[base_struct];
     }
   }
   else if(type.id() == ID_union_tag)

src/solvers/smt2/smt2_conv.h

@@ -209,8 +209,10 @@ class smt2_convt : public stack_decision_proceduret
 
   identifier_mapt identifier_map;
 
-  // for modeling structs as Z3 datatype, enabled when
-  // use_datatype is set
+  // for modeling structs as SMT datatype when use_datatype is set
+  //
+  // it maintains a map of `struct_typet` or `struct_tag_typet`
+  // to datatype names declared in SMT
   typedef std::map<typet, std::string> datatype_mapt;
   datatype_mapt datatype_map;