Add handling of "unknown" SMT outcome

Currently it is possible for z3 (and maybe other SMT solvers) to
return a satisfiability result of "unknown". At the moment this is
treated as an ERROR outcome in cbmc. This commit changes the
error message handling to output why the result was ERROR by
reporting the "unknown" satisfiability result.

Author: TGWDB

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)