Do not use as const with Z3 due to soundness issue

src/solvers/smt2/smt2_conv.cpp

@@ -118,7 +118,7 @@ smt2_convt::smt2_convt(
 
   case solvert::Z3:
     use_array_of_bool = true;
-    use_as_const = true;
+    use_as_const = false;
     use_check_sat_assuming = true;
     use_lambda_for_array = true;
     emit_set_logic = false;
@@ -5028,7 +5028,7 @@ void smt2_convt::unflatten(
   }
   else if(type.id() == ID_array)
   {
-    PRECONDITION(use_as_const);
+    PRECONDITION(use_as_const || use_lambda_for_array);
 
     if(where == wheret::BEGIN)
       out << "(let ((?ufop" << nesting << " ";
@@ -5049,9 +5049,23 @@ void smt2_convt::unflatten(
       for(mp_integer i = 1; i < size; ++i)
         out << "(store ";
 
-      out << "((as const ";
-      convert_type(array_type);
-      out << ") ";
+      // Build a constant array filled with element 0 as the base, then
+      // overwrite indices 1..N-1 via (store ...).
+      if(use_as_const)
+      {
+        out << "((as const ";
+        convert_type(array_type);
+        out << ") ";
+      }
+      else
+      {
+        // When `as const` is unavailable (e.g. Z3 due to a soundness
+        // issue), use a lambda that ignores its argument and returns the
+        // element-0 value. This is semantically equivalent to `as const`.
+        out << "(lambda ((?ufidx" << nesting << " ";
+        convert_type(array_type.index_type());
+        out << ")) ";
+      }
       // use element at index 0 as default value
       unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
       out << "((_ extract " << subtype_width - 1 << " "
@@ -5219,6 +5233,33 @@ void smt2_convt::set_to(const exprt &expr, bool value)
           convert_expr(prepared_rhs);
           out << ')' << ')' << '\n';
         }
+        else if(!use_as_const)
+        {
+          // When `as const` is unavailable, unflatten may emit lambda
+          // expressions. Z3 rejects `get-value` on symbols whose
+          // `define-fun` body contains lambdas, so we use
+          // `declare-fun` + `assert (= ...)` instead.
+          out << "(declare-fun " << smt2_identifier;
+          out << " () ";
+          convert_type(equal_expr.lhs().type());
+          out << ")\n";
+          out << "(assert (= " << smt2_identifier << ' ';
+          if(
+            equal_expr.lhs().type().id() != ID_array ||
+            use_array_theory(prepared_rhs))
+          {
+            convert_expr(prepared_rhs);
+          }
+          else
+          {
+            unflatten(wheret::BEGIN, equal_expr.lhs().type());
+
+            convert_expr(prepared_rhs);
+
+            unflatten(wheret::END, equal_expr.lhs().type());
+          }
+          out << "))\n";
+        }
         else
         {
           out << "(define-fun " << smt2_identifier;