Implement handling of success messages from SMT solver

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -18,6 +18,20 @@
 
 #include <stack>
 
+/// Issues a command to the solving process which is expected to optionally
+/// return a success status followed by response of interest.
+static smt_responset get_response_to_command(
+  smt_base_solver_processt &solver_process,
+  const smt_commandt &command)
+{
+  solver_process.send(smt_check_sat_commandt{});
+  auto response = solver_process.receive_response();
+  if(response.cast<smt_success_responset>())
+    return solver_process.receive_response();
+  else
+    return response;
+}
+
 /// \brief Find all sub expressions of the given \p expr which need to be
 ///   expressed as separate smt commands.
 /// \return A collection of sub expressions, which need to be expressed as
@@ -215,7 +229,8 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
   solver_process->send(smt_check_sat_commandt{});
-  const smt_responset result = solver_process->receive_response();
+  const smt_responset result =
+    get_response_to_command(*solver_process, smt_check_sat_commandt{});
   if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
   {
     if(check_sat_response->kind().cast<smt_unknown_responset>())

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -286,3 +286,11 @@ TEST_CASE(
     CHECK(test.procedure() == decision_proceduret::resultt::D_ERROR);
   }
 }
+
+TEST_CASE("smt2_incremental_decision_proceduret receives success and check-sat response.",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  test.mock_responses = {smt_success_responset{}, smt_check_sat_responset{smt_sat_responset{}}};
+  REQUIRE_NOTHROW(test.procedure());
+}