From c2ec649f15f866848f41ea142d77386174d8c8ed Mon Sep 17 00:00:00 2001
From: Saswat Padhi <saspadhi@amazon.com>
Date: Tue, 9 Mar 2021 14:56:30 -0500
Subject: [PATCH] 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.
---
 regression/cbmc/struct15/main.c    | 14 ++++++++++++++
 regression/cbmc/struct15/test.desc | 11 +++++++++++
 src/solvers/smt2/smt2_conv.cpp     |  4 +++-
 src/solvers/smt2/smt2_conv.h       |  6 ++++--
 4 files changed, 32 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/struct15/main.c
 create mode 100644 regression/cbmc/struct15/test.desc

diff --git a/regression/cbmc/struct15/main.c b/regression/cbmc/struct15/main.c
new file mode 100644
index 00000000000..f808a7979e5
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc/struct15/test.desc b/regression/cbmc/struct15/test.desc
new file mode 100644
index 00000000000..3faa87ff9fa
--- /dev/null
+++ b/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.
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 937f1ff298d..28a20744bbd 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/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)
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index 4de7056098c..22ab8480546 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/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;