diff --git a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc b/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc
index 6066f2b9402..484d5f5391d 100644
--- a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc
+++ b/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc
@@ -1,4 +1,4 @@
-CORE smt-backend no-new-smt
+KNOWNBUG smt-backend no-new-smt
 smt_missing_range_check.c
 --no-malloc-may-fail --pointer-check -z3
 ^EXIT=10$
@@ -9,7 +9,10 @@ smt_missing_range_check.c
 --
 --
 Check that memory checks fail for pointer dereferences inside an existential
-qualifier, for out of bounds memory access, when using the smt backend and
+quantifier, for out of bounds memory access, when using the smt backend and
 the range of the index is unbound. Note that this test is not expected to work
 with the SAT backend at the time of writing, as the SAT backend does not support
-qualifiers in this form.
+quantifiers in this form.
+
+Neither Z3 nor CVC5 currently return complete models, and Bitwuzla does not
+complete in more than 5 minutes.
diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp
index 19f57ab9a55..605d82bf61b 100644
--- a/src/solvers/smt2/smt2_dec.cpp
+++ b/src/solvers/smt2/smt2_dec.cpp
@@ -236,22 +236,45 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
   {
     const std::string boolean_identifier =
       convert_identifier("B" + std::to_string(v));
-    boolean_assignment[v] = [&]() {
       const auto found_parsed_value =
         parsed_values.find(drop_quotes(boolean_identifier));
       if(found_parsed_value != parsed_values.end())
       {
-        return found_parsed_value->second.id() == ID_true;
+        const irept &value = found_parsed_value->second;
+
+        if(value.id() != ID_true && value.id() != ID_false)
+        {
+          messaget log{message_handler};
+          log.error() << "SMT2 solver returned non-Boolean value for variable "
+                      << boolean_identifier << messaget::eom;
+          return decision_proceduret::resultt::D_ERROR;
+        }
+        boolean_assignment[v] = value.id() == ID_true;
+      }
+      else
+      {
+        // Work out the value based on what set_to was called with.
+        const auto found_set_value = set_values.find(boolean_identifier);
+        if(found_set_value != set_values.end())
+          boolean_assignment[v] = found_set_value->second;
+        else
+        {
+          // Old code used the computation
+          // const irept &value=values["B"+std::to_string(v)];
+          // boolean_assignment[v]=(value.id()==ID_true);
+          const irept &value = parsed_values[boolean_identifier];
+
+          if(value.id() != ID_true && value.id() != ID_false)
+          {
+            messaget log{message_handler};
+            log.error()
+              << "SMT2 solver returned non-Boolean value for variable "
+              << boolean_identifier << messaget::eom;
+            return decision_proceduret::resultt::D_ERROR;
+          }
+          boolean_assignment[v] = value.id() == ID_true;
+        }
       }
-      // Work out the value based on what set_to was called with.
-      const auto found_set_value = set_values.find(boolean_identifier);
-      if(found_set_value != set_values.end())
-        return found_set_value->second;
-      // Old code used the computation
-      // const irept &value=values["B"+std::to_string(v)];
-      // boolean_assignment[v]=(value.id()==ID_true);
-      return parsed_values[boolean_identifier].id() == ID_true;
-    }();
   }
 
   return res;