Implement getting arrays from the SMT2 backend

This was previously unimplemented, which put null expressions into the
trace steps and resulted in the elements of arrays not being printed
when the trace is printed.

Author: thomasspriggs

src/solvers/smt2/smt2_conv.cpp

@@ -318,6 +318,15 @@ exprt smt2_convt::get(const exprt &expr) const
   }
   else if(expr.is_constant())
     return expr;
+  else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
+  {
+    exprt array_copy = *array;
+    for(auto &element : array_copy.operands())
+    {
+      element = get(element);
+    }
+    return array_copy;
+  }
 
   return nil_exprt();
 }