Fixed SMT encoding of array_of_exprt

Instead of using quantifers to encode array_of expressions -- which, as indicated in the comments, doesn't seem to work on existing solvers -- we can use the `as const` construct.

Author: SaswatPadhi

src/solvers/smt2/smt2_conv.cpp

@@ -4367,27 +4367,23 @@ void smt2_convt::find_symbols(const exprt &expr)
       out << ")" << "\n";
     }
   }
-  else if(expr.id()==ID_array_of)
+  else if(expr.id() == ID_array_of)
   {
-    if(defined_expressions.find(expr)==defined_expressions.end())
+    if(defined_expressions.find(expr) == defined_expressions.end())
     {
+      const array_of_exprt &array_of_expr = to_array_of_expr(expr);
+
       const irep_idt id =
         "array_of." + std::to_string(defined_expressions.size());
-      out << "; the following is a substitute for lambda i. x" << "\n";
-      out << "(declare-fun " << id << " () ";
-      convert_type(expr.type());
-      out << ")" << "\n";
-
-      // use a quantifier instead of the lambda
-      #if 0 // not really working in any solver yet!
-      out << "(assert (forall ((i ";
-      convert_type(array_index_type());
-      out << ")) (= (select " << id << " i) ";
-      convert_expr(expr.op0());
-      out << ")))" << "\n";
-      #endif
+      out << "(define-fun " << id << " () ";
+      convert_type(array_of_expr.type());
+      out << " ((as const ";
+      convert_type(array_of_expr.type());
+      out << ") ";
+      convert_expr(array_of_expr.what());
+      out << "))\n";
 
-      defined_expressions[expr]=id;
+      defined_expressions[expr] = id;
     }
   }
   else if(expr.id()==ID_array)