Follow struct-tag before accessing is smt2 datatype

in smt2-conversion. Before std::map threw exception at 'at' (since we follow the
tag before inserting the converted datatype). Includes a regression test.

Author: petr-bauch

regression/cbmc/Struct_Hack_Initialization_SMT2/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+typedef struct stritem
+{
+  unsigned nkey;
+  unsigned cas[];
+} item;
+
+int foo(item *it)
+{
+  assert(it->cas[0] == 0);
+  return 0;
+}

regression/cbmc/Struct_Hack_Initialization_SMT2/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--function foo --bounds-check --pointer-check --smt2
+^\[foo.assertion.1\] line \d+ assertion it->cas\[0\] == 0: FAILURE$
+^\[foo.array_bounds.3\] line \d+ array.cas upper bound in it->cas\[\(.*\)0\]: FAILURE$
+^\[foo.array_bounds.2\] line \d+ array.cas dynamic object upper bound in it->cas\[\(.*\)0\]: FAILURE$
+^\[foo.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in it->cas: SUCCESS$
+^\[foo.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in it->cas: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/solvers/smt2/smt2_conv.cpp

@@ -4533,7 +4533,11 @@ void smt2_convt::convert_type(const typet &type)
   {
     if(use_datatypes)
     {
-      out << datatype_map.at(type);
+      const typet &struct_type = type.id() == ID_struct_tag
+                                   ? ns.follow_tag(to_struct_tag_type(type))
+                                   : type;
+      CHECK_RETURN(datatype_map.count(struct_type) > 0);
+      out << datatype_map.at(struct_type);
     }
     else
     {