SMT back-end: fix parsing of Z3 models involving let

Z3 produces models such as
```
((|main::1::arr!0@1#3[[1]]| (let ((a!1 (store (store (store ((as const (Array (_ BitVec 64) (_ BitVec 8)))
                                  #x00)
                                #x0000000000000003
                                #x02)
                         #x0000000000000002
                         #x01)
                  #x0000000000000004
                  #x01)))
  (mk-struct.0 #x00 #x00 a!1))))
```
(for cbmc/Array_operations2), which is a `let` around a struct. Our code
previously would only handle these for arrays, and not for arrays within
other compound types. Also, Z3 may use multiple bindings (observable in
the same regression test), which we did not cater for at all.

This commit promotes `let` parsing to the top level, expanding bindings
as needed.

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -537,14 +537,6 @@ void smt2_convt::walk_array_tree(
     exprt value = parse_rec(src.get_sub()[3], type.element_type());
     operands_map->emplace(index, value);
   }
-  else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let")
-  {
-    // This is produced by Z3
-    // (let (....) (....))
-    walk_array_tree(
-      operands_map, src.get_sub()[1].get_sub()[0].get_sub()[1], type);
-    walk_array_tree(operands_map, src.get_sub()[2], type);
-  }
   else if(src.get_sub().size()==2 &&
           src.get_sub()[0].get_sub().size()==3 &&
           src.get_sub()[0].get_sub()[0].id()=="as" &&
@@ -554,6 +546,12 @@ void smt2_convt::walk_array_tree(
     exprt default_value = parse_rec(src.get_sub()[1], type.element_type());
     operands_map->emplace(-1, default_value);
   }
+  else
+  {
+    auto bindings_it = current_bindings.find(src.id());
+    if(bindings_it != current_bindings.end())
+      walk_array_tree(operands_map, bindings_it->second, type);
+  }
 }
 
 exprt smt2_convt::parse_union(
@@ -633,6 +631,27 @@ smt2_convt::parse_struct(const irept &src, const struct_typet &type)
 
 exprt smt2_convt::parse_rec(const irept &src, const typet &type)
 {
+  if(src.get_sub().size() == 3 && src.get_sub()[0].id() == ID_let)
+  {
+    // This is produced by Z3
+    // (let (....) (....))
+    auto previous_bindings = current_bindings;
+    for(const auto &binding : src.get_sub()[1].get_sub())
+    {
+      const irep_idt &name = binding.get_sub()[0].id();
+      current_bindings.emplace(name, binding.get_sub()[1]);
+    }
+    exprt result = parse_rec(src.get_sub()[2], type);
+    current_bindings = std::move(previous_bindings);
+    return result;
+  }
+
+  auto bindings_it = current_bindings.find(src.id());
+  if(bindings_it != current_bindings.end())
+  {
+    return parse_rec(bindings_it->second, type);
+  }
+
   if(
     type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
     type.id() == ID_integer || type.id() == ID_rational ||

src/solvers/smt2/smt2_conv.h

@@ -187,6 +187,7 @@ class smt2_convt : public stack_decision_proceduret
     std::unordered_map<int64_t, exprt> *operands_map,
     const irept &src,
     const array_typet &type);
+  std::unordered_map<irep_idt, irept> current_bindings;
 
   // we use this to build a bit-vector encoding of the FPA theory
   void convert_floatbv(const exprt &expr);