diff --git a/regression/cbmc/Malloc22/test.desc b/regression/cbmc/Malloc22/test.desc
index 11c11d90c5c..72f4c319ba9 100644
--- a/regression/cbmc/Malloc22/test.desc
+++ b/regression/cbmc/Malloc22/test.desc
@@ -1,7 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --unwind 2 --smt2 --outfile main.smt2
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^Invalid expression: failed to get width of byte_update
+--
+20220523: Marked as KNOWNBUG due to encoding into some solvers not being
+done correctly. This works for z3 and cvc4, but not other solvers.
diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
index ae228a04e44..eac1d35ee1e 100644
--- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
+++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --smt2 --outfile -
 \(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
@@ -11,6 +11,10 @@ main.c
 \(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
 \(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
 --
+20220523: Marked as KNOWNBUG due to encoding into some solvers not being
+done correctly. This works for z3 and cvc4, but not other solvers. Old
+comments below.
+
 This test checks for correctness of BitVec-array encoding of Boolean arrays.
 
 Ideally, we shouldn't have to check the SMT output, but should run with backend
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index e477ff77607..9ad3f68a41b 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4721,21 +4721,36 @@ 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.element_type().id() == ID_bool && !use_array_of_bool)
+        // 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)
         {
-          out << "(ite ";
-          convert_expr(array_of.what());
-          out << " #b1 #b0)";
+          // 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.element_type().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";
         }
         else
         {
-          convert_expr(array_of.what());
+          // This is where an alternate for other solvers that does not use
+          // quantifiers should go.
+          INVARIANT(
+            false,
+            "Cannot substitute quantified expression for lambda in current "
+            "solver.");
         }
-        out << ")))\n";
 
         defined_expressions[expr] = id;
       }