Implement error messaging for invalid SMT responses

Author: thomasspriggs

src/solvers/smt2_incremental/smt_response_validation.cpp

@@ -48,5 +48,6 @@ response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
       smt_check_sat_responset{smt_unknown_responset{}}};
   if(parse_tree.id() == "success")
     return response_or_errort<smt_responset>{smt_success_responset{}};
-  UNIMPLEMENTED;
+  return response_or_errort<smt_responset>{"Invalid SMT response \"" +
+                                           id2string(parse_tree.id()) + "\""};
 }

unit/solvers/smt2_incremental/smt_response_validation.cpp

@@ -50,3 +50,20 @@ TEST_CASE("Validation of SMT success response", "[core][smt2_incremental]")
     *validate_smt_response(*smt2irep("success").parsed_output).get_if_valid() ==
     smt_success_responset{});
 }
+
+TEST_CASE(
+  "Error handling of SMT response validation",
+  "[core][smt2_incremental]")
+{
+  SECTION("Parse tree produced is not a valid SMT-LIB version 2.6 response")
+  {
+    const response_or_errort<smt_responset> validation_response =
+      validate_smt_response(*smt2irep("foobar").parsed_output);
+    CHECK(
+      *validation_response.get_if_error() ==
+      std::vector<std::string>{"Invalid SMT response \"foobar\""});
+    CHECK(
+      *validate_smt_response(*smt2irep("()").parsed_output).get_if_error() ==
+      std::vector<std::string>{"Invalid SMT response \"\""});
+  }
+}