Merge pull request #6221 from TGWDB/SMT-unknown-handling

Smt unknown handling

Author: kroening

regression/cbmc/z3/Issue5977.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void main()
+{
+  int i;
+  __CPROVER_assume(i % 2 == 0);
+  assert(__CPROVER_exists {
+    int j;
+    i == j + j
+  });
+}

regression/cbmc/z3/Issue5977.desc

@@ -0,0 +1,9 @@
+CORE smt-backend broken-cprover-smt-backend
+Issue5977.c
+--z3
+^EXIT=(6|10)$
+^SIGNAL=0$
+^SMT2 solver returned "unknown"$
+--
+--
+This tests that an "unknown" result from the SMT solver is reported.

src/solvers/smt2/smt2_dec.cpp

@@ -154,6 +154,12 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
       res=resultt::D_SATISFIABLE;
     else if(parsed.id()=="unsat")
       res=resultt::D_UNSATISFIABLE;
+    else if(parsed.id() == "unknown")
+    {
+      messaget log{message_handler};
+      log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
+      return decision_proceduret::resultt::D_ERROR;
+    }
     else if(
       parsed.id().empty() && parsed.get_sub().size() == 1 &&
       parsed.get_sub().front().get_sub().size() == 2)