Fix quantifiers for arrays only works with Z3 and CVC4

This commit fixes an error introduced in diffblue#5974 where quantifiers
were produced for all SMT2 solvers despite only being supported by
Z3 and CVC4. The fix here reverts to the older behaviour for other
solvers.

Fixes diffblue#6263

Author: TGWDB

src/solvers/smt2/smt2_conv.cpp

@@ -4552,21 +4552,32 @@ void smt2_convt::find_symbols(const exprt &expr)
         convert_type(array_type);
         out << ")\n";
 
-        // use a quantifier-based initialization instead of lambda
-        out << "(assert (forall ((i ";
-        convert_type(array_type.size().type());
-        out << ")) (= (select " << id << " i) ";
-        if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
-        {
-          out << "(ite ";
-          convert_expr(array_of.what());
-          out << " #b1 #b0)";
-        }
-        else
+        // The code below only works in Z3 and CVC4, it was added (and
+        // approved/merged) despite breaking other solvers.
+        // This conditional removes this for other solvers
+        if(solver == solvert::CVC4 || solver == solvert::Z3)
         {
-          convert_expr(array_of.what());
+          // use a quantifier-based initialization instead of lambda
+          out << "(assert (forall ((i ";
+          convert_type(array_type.size().type());
+          out << ")) (= (select " << id << " i) ";
+          if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
+          {
+            out << "(ite ";
+            convert_expr(array_of.what());
+            out << " #b1 #b0)";
+          }
+          else
+          {
+            convert_expr(array_of.what());
+          }
+          out << ")))\n";
         }
-        out << ")))\n";
+        // else
+        // {
+        //   // This is where an alternate for other solvers that does not use
+        //   // quantifiers should go.
+        // }
 
         defined_expressions[expr] = id;
       }