From 2ec49740427b40eb4831e1da1c99b71cc3b57d77 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 12 Jul 2024 11:02:21 +0000
Subject: [PATCH] SMT2 back-end: detect when solver returns unexpected model

We have seen examples of Z3 responding with
```
((B1502 (forall ((|main::tmp_cc$0!0@1#0| (_ BitVec 64)))
  (let ((a!1 (or (and (not (bvule #x000000000000000c |main::tmp_cc$0!0@1#0|))
                      (bvule #x000000000000000b |main::tmp_cc$0!0@1#0|)
[...]
```
when we expected just `true` or `false` as model (which Bitwuzla seemed
to get right on the very same input program). Report these as errors
rather than using the incomplete assignment. Such an incomplete
assignment would make us re-try forever without making progress.

Fixes: #8365
---
 .../smt_missing_range_check.desc              |  9 ++--
 src/solvers/smt2/smt2_dec.cpp                 | 45 ++++++++++++++-----
 2 files changed, 40 insertions(+), 14 deletions(-)

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;