Add regression test for missing lowering in new SMT backend

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/structs/struct_static_init.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdint.h>
+
+struct F
+{
+  uint16_t w;
+  uint16_t x;
+};
+
+static struct F a = {0xdeadbeef};
+static struct F b = {0xbeefdead};
+
+int main()
+{
+  struct F *p;
+  if(nondet_int())
+    p = &a;
+  else
+    p = &b;
+
+  assert(p->w != 0xdead);
+}

regression/cbmc-incr-smt2/structs/struct_static_init.desc

@@ -0,0 +1,11 @@
+CORE
+struct_static_init.c
+
+Passing problem to incremental SMT2 solving
+line \d+ assertion p->w != 0xdead: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that statically initialised variables of struct type (whose values are
+stored in the symbolt_table) are lowered correctly.