Merge pull request #8379 from tautschnig/bugfixes/smt2-value-check-8365

SMT2 back-end: detect when solver returns unexpected model

Author: tautschnig

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.

regression/cbmc/Quantifiers-assertion/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE broken-z3-smt-backend no-new-smt
 main.c
 
 ^\*\* Results:$

regression/cbmc/z3/Issue5977.desc

@@ -3,7 +3,7 @@ Issue5977.c
 --z3
 ^EXIT=(6|10)$
 ^SIGNAL=0$
-^SMT2 solver returned "unknown"$
+^SMT2 solver returned ("unknown"|non-constant value for variable B\d+)$
 --
 --
 This tests that an "unknown" result from the SMT solver is reported.

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-constant 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;