diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.c b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.c
new file mode 100644
index 00000000000..e0111538977
--- /dev/null
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.c
@@ -0,0 +1,12 @@
+
+int main()
+{
+  int x;
+  int y;
+  if(y)
+    y = x;
+  else
+    y = x;
+  __CPROVER_assert(y == x, "Nondeterministic int assert.");
+  return 0;
+}
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc
new file mode 100644
index 00000000000..93f93857cd7
--- /dev/null
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc
@@ -0,0 +1,14 @@
+CORE winbug
+valid_unsat.c
+--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Sending command to SMT2 solver - \(check-sat\)
+Solver response - unsat
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+type: pointer
+--
+Test that given a `.c` program where all assertions hold, the solver responds
+with unsat and CBMC reports that verification is successful.
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 7a9cdadb37d..49d4bea5a4b 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -5,10 +5,12 @@
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_responses.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <util/expr.h>
 #include <util/namespace.h>
+#include <util/nodiscard.h>
 #include <util/range.h>
 #include <util/std_expr.h>
 #include <util/string_utils.h>
@@ -16,6 +18,35 @@
 
 #include <stack>
 
+/// Issues a command to the solving process which is expected to optionally
+/// return a success status followed by the actual response of interest.
+static smt_responset get_response_to_command(
+  smt_base_solver_processt &solver_process,
+  const smt_commandt &command)
+{
+  solver_process.send(command);
+  auto response = solver_process.receive_response();
+  if(response.cast<smt_success_responset>())
+    return solver_process.receive_response();
+  else
+    return response;
+}
+
+static optionalt<std::string>
+get_problem_messages(const smt_responset &response)
+{
+  if(const auto error = response.cast<smt_error_responset>())
+  {
+    return "SMT solver returned an error message - " +
+           id2string(error->message());
+  }
+  if(response.cast<smt_unsupported_responset>())
+  {
+    return {"SMT solver does not support given command."};
+  }
+  return {};
+}
+
 /// \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
@@ -196,10 +227,31 @@ void smt2_incremental_decision_proceduret::pop()
   UNIMPLEMENTED_FEATURE("`pop`.");
 }
 
+NODISCARD
+static decision_proceduret::resultt lookup_decision_procedure_result(
+  const smt_check_sat_response_kindt &response_kind)
+{
+  if(response_kind.cast<smt_sat_responset>())
+    return decision_proceduret::resultt::D_SATISFIABLE;
+  if(response_kind.cast<smt_unsat_responset>())
+    return decision_proceduret::resultt::D_UNSATISFIABLE;
+  if(response_kind.cast<smt_unknown_responset>())
+    return decision_proceduret::resultt::D_ERROR;
+  UNREACHABLE;
+}
+
 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();
-  UNIMPLEMENTED_FEATURE("handling solver 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>())
+      log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
+    return lookup_decision_procedure_result(check_sat_response->kind());
+  }
+  if(const auto problem = get_problem_messages(result))
+    throw analysis_exceptiont{*problem};
+  throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
 }
diff --git a/src/solvers/smt2_incremental/smt_response_validation.h b/src/solvers/smt2_incremental/smt_response_validation.h
index 9dd8295f27b..81b3d8f411b 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.h
+++ b/src/solvers/smt2_incremental/smt_response_validation.h
@@ -5,6 +5,7 @@
 
 #include <solvers/smt2_incremental/smt_responses.h>
 #include <util/invariant.h>
+#include <util/nodiscard.h>
 #include <util/optional.h>
 
 #include <string>
@@ -37,7 +38,7 @@ class response_or_errort final
   std::vector<std::string> messages;
 };
 
-response_or_errort<smt_responset>
+NODISCARD response_or_errort<smt_responset>
 validate_smt_response(const irept &parse_tree);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
diff --git a/src/solvers/smt2_incremental/smt_solver_process.cpp b/src/solvers/smt2_incremental/smt_solver_process.cpp
index 148aefbf259..514b4d73da1 100644
--- a/src/solvers/smt2_incremental/smt_solver_process.cpp
+++ b/src/solvers/smt2_incremental/smt_solver_process.cpp
@@ -2,7 +2,10 @@
 
 #include <solvers/smt2_incremental/smt_solver_process.h>
 
+#include <solvers/smt2/smt2irep.h>
+#include <solvers/smt2_incremental/smt_response_validation.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/string_utils.h>
 
@@ -28,9 +31,28 @@ void smt_piped_solver_processt::send(const smt_commandt &smt_command)
   process.send(command_string + "\n");
 }
 
+/// Log messages and throw exception.
+static void handle_invalid_smt(
+  const std::vector<std::string> &validation_errors,
+  messaget &log)
+{
+  for(const std::string &message : validation_errors)
+  {
+    log.error() << message << messaget::eom;
+  }
+  throw analysis_exceptiont{"Invalid SMT response received from solver."};
+}
+
 smt_responset smt_piped_solver_processt::receive_response()
 {
   const auto response_text = process.wait_receive();
   log.debug() << "Solver response - " << response_text << messaget::eom;
-  UNIMPLEMENTED_FEATURE("parsing of solver response.");
+  response_stream << response_text;
+  const auto parse_tree = smt2irep(response_stream, log.get_message_handler());
+  if(!parse_tree)
+    throw deserialization_exceptiont{"Incomplete SMT response."};
+  const auto validation_result = validate_smt_response(*parse_tree);
+  if(const auto validation_errors = validation_result.get_if_error())
+    handle_invalid_smt(*validation_errors, log);
+  return *validation_result.get_if_valid();
 }
diff --git a/src/solvers/smt2_incremental/smt_solver_process.h b/src/solvers/smt2_incremental/smt_solver_process.h
index de094f13b01..3c174b486b0 100644
--- a/src/solvers/smt2_incremental/smt_solver_process.h
+++ b/src/solvers/smt2_incremental/smt_solver_process.h
@@ -9,6 +9,7 @@ class smt_commandt;
 #include <util/message.h>
 #include <util/piped_process.h>
 
+#include <sstream>
 #include <string>
 
 class smt_base_solver_processt
@@ -49,6 +50,8 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   std::string command_line_description;
   /// The raw solver sub process.
   piped_processt process;
+  /// For buffering / combining communications from the solver to cbmc.
+  std::stringstream response_stream;
   /// For debug printing.
   messaget log;
 };
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 13444d7b121..047407fefb6 100644
--- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -5,11 +5,13 @@
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_responses.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/exception_utils.h>
 #include <util/make_unique.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
@@ -20,9 +22,51 @@
 // appropriate overload of `operator<<` where it exists.
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 
+#include <deque>
+
+class analysis_execption_with_messaget
+  : public Catch::MatcherBase<analysis_exceptiont>
+{
+public:
+  explicit analysis_execption_with_messaget(std::string message);
+  bool match(const analysis_exceptiont &exception) const override;
+  std::string describe() const override;
+
+private:
+  std::string expected;
+};
+
+analysis_execption_with_messaget::analysis_execption_with_messaget(
+  std::string message)
+  : expected{std::move(message)}
+{
+}
+
+bool analysis_execption_with_messaget::match(
+  const analysis_exceptiont &exception) const
+{
+  return expected == exception.what();
+}
+
+std::string analysis_execption_with_messaget::describe() const
+{
+  return std::string{"analysis_exceptiont with `.what' containing - \""} +
+         expected + "\"";
+}
+
 class smt_mock_solver_processt : public smt_base_solver_processt
 {
+  std::function<void(const smt_commandt &)> _send;
+  std::function<smt_responset()> _receive;
+
 public:
+  smt_mock_solver_processt(
+    std::function<void(const smt_commandt &)> send,
+    std::function<smt_responset()> receive)
+    : _send{std::move(send)}, _receive{std::move(receive)}
+  {
+  }
+
   const std::string &description() override
   {
     UNREACHABLE;
@@ -30,19 +74,49 @@ class smt_mock_solver_processt : public smt_base_solver_processt
 
   void send(const smt_commandt &smt_command) override
   {
-    sent_commands.push_back(smt_command);
+    _send(smt_command);
   }
 
   smt_responset receive_response() override
   {
-    UNREACHABLE;
+    return _receive();
   }
 
-  std::vector<smt_commandt> sent_commands;
-
   ~smt_mock_solver_processt() override = default;
 };
 
+struct decision_procedure_test_environmentt final
+{
+  void send(const smt_commandt &smt_command);
+  smt_responset receive_response();
+
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  std::deque<smt_responset> mock_responses;
+  std::vector<smt_commandt> sent_commands;
+  null_message_handlert message_handler;
+  smt2_incremental_decision_proceduret procedure{
+    ns,
+    util_make_unique<smt_mock_solver_processt>(
+      [&](const smt_commandt &smt_command) { this->send(smt_command); },
+      [&]() { return this->receive_response(); }),
+    message_handler};
+};
+
+void decision_procedure_test_environmentt::send(const smt_commandt &smt_command)
+{
+  sent_commands.push_back(smt_command);
+}
+
+smt_responset decision_procedure_test_environmentt::receive_response()
+{
+  INVARIANT(
+    !mock_responses.empty(), "There must be responses remaining for test.");
+  smt_responset response = mock_responses.front();
+  mock_responses.pop_front();
+  return response;
+}
+
 static symbolt make_test_symbol(irep_idt id, typet type)
 {
   symbolt new_symbol;
@@ -64,29 +138,23 @@ TEST_CASE(
   "smt2_incremental_decision_proceduret commands sent",
   "[core][smt2_incremental]")
 {
-  symbol_tablet symbol_table;
-  namespacet ns{symbol_table};
-  auto mock_process = util_make_unique<smt_mock_solver_processt>();
-  auto &sent_commands = mock_process->sent_commands;
-  null_message_handlert message_handler;
+  decision_procedure_test_environmentt test{};
   SECTION("Construction / solver initialisation.")
   {
-    smt2_incremental_decision_proceduret procedure{
-      ns, std::move(mock_process), message_handler};
     REQUIRE(
-      sent_commands ==
+      test.sent_commands ==
       std::vector<smt_commandt>{
         smt_set_option_commandt{smt_option_produce_modelst{true}},
         smt_set_logic_commandt{
           smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}}});
-    sent_commands.clear();
+    test.sent_commands.clear();
     SECTION("Set symbol to true.")
     {
       const symbolt foo = make_test_symbol("foo", bool_typet{});
       const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
-      procedure.set_to(foo.symbol_expr(), true);
+      test.procedure.set_to(foo.symbol_expr(), true);
       REQUIRE(
-        sent_commands ==
+        test.sent_commands ==
         std::vector<smt_commandt>{smt_declare_function_commandt{foo_term, {}},
                                   smt_assert_commandt{foo_term}});
     }
@@ -94,9 +162,9 @@ TEST_CASE(
     {
       const symbolt foo = make_test_symbol("foo", bool_typet{});
       const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
-      procedure.set_to(foo.symbol_expr(), false);
+      test.procedure.set_to(foo.symbol_expr(), false);
       REQUIRE(
-        sent_commands ==
+        test.sent_commands ==
         std::vector<smt_commandt>{
           smt_declare_function_commandt{foo_term, {}},
           smt_assert_commandt{smt_core_theoryt::make_not(foo_term)}});
@@ -105,43 +173,43 @@ TEST_CASE(
     {
       const symbolt forty_two =
         make_test_symbol("forty_two", from_integer({42}, signedbv_typet{16}));
-      symbol_table.insert(forty_two);
+      test.symbol_table.insert(forty_two);
       const smt_identifier_termt forty_two_term{"forty_two",
                                                 smt_bit_vector_sortt{16}};
       const symbolt nondet_int_a =
         make_test_symbol("nondet_int_a", signedbv_typet{16});
-      symbol_table.insert(nondet_int_a);
+      test.symbol_table.insert(nondet_int_a);
       const smt_identifier_termt nondet_int_a_term{"nondet_int_a",
                                                    smt_bit_vector_sortt{16}};
       const symbolt nondet_int_b =
         make_test_symbol("nondet_int_b", signedbv_typet{16});
-      symbol_table.insert(nondet_int_b);
+      test.symbol_table.insert(nondet_int_b);
       const smt_identifier_termt nondet_int_b_term{"nondet_int_b",
                                                    smt_bit_vector_sortt{16}};
       const symbolt first_comparison = make_test_symbol(
         "first_comparison",
         equal_exprt{nondet_int_a.symbol_expr(), forty_two.symbol_expr()});
-      symbol_table.insert(first_comparison);
+      test.symbol_table.insert(first_comparison);
       const symbolt second_comparison = make_test_symbol(
         "second_comparison",
         not_exprt{
           equal_exprt{nondet_int_b.symbol_expr(), forty_two.symbol_expr()}});
-      symbol_table.insert(second_comparison);
+      test.symbol_table.insert(second_comparison);
       const symbolt third_comparison = make_test_symbol(
         "third_comparison",
         equal_exprt{nondet_int_a.symbol_expr(), nondet_int_b.symbol_expr()});
-      symbol_table.insert(third_comparison);
+      test.symbol_table.insert(third_comparison);
       const symbolt comparison_conjunction = make_test_symbol(
         "comparison_conjunction",
         and_exprt{{first_comparison.symbol_expr(),
                    second_comparison.symbol_expr(),
                    third_comparison.symbol_expr()}});
-      symbol_table.insert(comparison_conjunction);
+      test.symbol_table.insert(comparison_conjunction);
       smt_identifier_termt comparison_conjunction_term{"comparison_conjunction",
                                                        smt_bool_sortt{}};
-      procedure.set_to(comparison_conjunction.symbol_expr(), true);
+      test.procedure.set_to(comparison_conjunction.symbol_expr(), true);
       REQUIRE(
-        sent_commands ==
+        test.sent_commands ==
         std::vector<smt_commandt>{
           smt_declare_function_commandt{nondet_int_a_term, {}},
           smt_define_function_commandt{
@@ -174,22 +242,24 @@ TEST_CASE(
     {
       const symbolt foo = make_test_symbol("foo", bool_typet{});
       const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
-      procedure.handle(foo.symbol_expr());
+      test.procedure.handle(foo.symbol_expr());
       REQUIRE(
-        sent_commands == std::vector<smt_commandt>{
-                           smt_declare_function_commandt{foo_term, {}},
-                           smt_define_function_commandt{"B0", {}, foo_term}});
-      sent_commands.clear();
+        test.sent_commands ==
+        std::vector<smt_commandt>{
+          smt_declare_function_commandt{foo_term, {}},
+          smt_define_function_commandt{"B0", {}, foo_term}});
+      test.sent_commands.clear();
       SECTION("Handle of previously handled expression.")
       {
-        procedure.handle(foo.symbol_expr());
-        REQUIRE(sent_commands.empty());
+        test.procedure.handle(foo.symbol_expr());
+        REQUIRE(test.sent_commands.empty());
       }
       SECTION("Handle of new expression containing previously defined symbol.")
       {
-        procedure.handle(equal_exprt{foo.symbol_expr(), foo.symbol_expr()});
+        test.procedure.handle(
+          equal_exprt{foo.symbol_expr(), foo.symbol_expr()});
         REQUIRE(
-          sent_commands ==
+          test.sent_commands ==
           std::vector<smt_commandt>{smt_define_function_commandt{
             "B1", {}, smt_core_theoryt::equal(foo_term, foo_term)}});
       }
@@ -198,10 +268,10 @@ TEST_CASE(
     {
       const symbolt bar =
         make_test_symbol("bar", from_integer({42}, signedbv_typet{8}));
-      symbol_table.insert(bar);
-      procedure.handle(bar.symbol_expr());
+      test.symbol_table.insert(bar);
+      test.procedure.handle(bar.symbol_expr());
       REQUIRE(
-        sent_commands ==
+        test.sent_commands ==
         std::vector<smt_commandt>{
           smt_define_function_commandt{
             "bar", {}, smt_bit_vector_constant_termt{42, 8}},
@@ -210,3 +280,101 @@ TEST_CASE(
     }
   }
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret number of solver calls.",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  REQUIRE(test.procedure.get_number_of_solver_calls() == 0);
+  test.mock_responses.push_back(smt_check_sat_responset{smt_unsat_responset{}});
+  test.procedure();
+  REQUIRE(test.procedure.get_number_of_solver_calls() == 1);
+  test.mock_responses.push_back(smt_check_sat_responset{smt_unsat_responset{}});
+  test.procedure();
+  REQUIRE(test.procedure.get_number_of_solver_calls() == 2);
+}
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret mapping solver check-sat responses to "
+  "internal decision_proceduret::resultt",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  SECTION("sat")
+  {
+    test.mock_responses = {smt_check_sat_responset{smt_sat_responset{}}};
+    CHECK(test.procedure() == decision_proceduret::resultt::D_SATISFIABLE);
+  }
+  SECTION("unsat")
+  {
+    test.mock_responses = {smt_check_sat_responset{smt_unsat_responset{}}};
+    CHECK(test.procedure() == decision_proceduret::resultt::D_UNSATISFIABLE);
+  }
+  SECTION("unknown")
+  {
+    test.mock_responses = {smt_check_sat_responset{smt_unknown_responset{}}};
+    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{};
+  SECTION("Expected success response.")
+  {
+    test.mock_responses = {smt_success_responset{},
+                           smt_check_sat_responset{smt_sat_responset{}}};
+    REQUIRE_NOTHROW(test.procedure());
+  }
+  SECTION("Duplicated success messages.")
+  {
+    test.mock_responses = {smt_success_responset{},
+                           smt_success_responset{},
+                           smt_check_sat_responset{smt_sat_responset{}}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "Unexpected kind of response from SMT solver."});
+  }
+}
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret receives unexpected responses to "
+  "check-sat.",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  SECTION("get-value response")
+  {
+    test.mock_responses = {
+      smt_get_value_responset{{{"x", smt_bool_literal_termt{false}}}}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "Unexpected kind of response from SMT solver."});
+  }
+  SECTION("error message response")
+  {
+    test.mock_responses = {smt_error_responset{"foobar"}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "SMT solver returned an error message - foobar"});
+  }
+  SECTION("unsupported response")
+  {
+    test.mock_responses = {smt_unsupported_responset{}};
+    REQUIRE_THROWS_MATCHES(
+      test.procedure(),
+      analysis_exceptiont,
+      analysis_execption_with_messaget{
+        "SMT solver does not support given command."});
+  }
+}