From e5676aff0348bd4fd08665babcef14d9ab53de5d Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:13 +0100
Subject: [PATCH 01/18] Make decision procedure use piped solver

---
 .../smt2_incremental_decision_procedure.cpp        | 14 ++++++++++++--
 .../smt2_incremental_decision_procedure.h          |  8 ++++++++
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index a62c140575b..046aec27ce0 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -2,11 +2,15 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
+#include <util/string_utils.h>
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
-  std::string solver_command)
-  : solver_command{std::move(solver_command)}, number_of_solver_calls{0}
+  std::string _solver_command)
+  : solver_command{std::move(_solver_command)},
+    number_of_solver_calls{0},
+    solver_process{split_string(solver_command, ' ', false, true)}
 {
 }
 
@@ -71,3 +75,9 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
   ++number_of_solver_calls;
   UNIMPLEMENTED_FEATURE("solving.");
 }
+
+void smt2_incremental_decision_proceduret::send_to_solver(
+  const smt_commandt &command)
+{
+  solver_process.send(smt_to_smt2_string(command) + "\n");
+}
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index b1caed2e64d..51504f623c8 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -7,6 +7,9 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
 #include <solvers/stack_decision_procedure.h>
+#include <util/piped_process.h>
+
+class smt_commandt;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
@@ -32,10 +35,15 @@ class smt2_incremental_decision_proceduret final
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
+  /// \brief Converts given SMT2 command to SMT2 string and sends it to the
+  ///    solver process.
+  void send_to_solver(const smt_commandt &command);
 
   /// This is where we store the solver command for reporting the solver used.
   std::string solver_command;
   size_t number_of_solver_calls;
+
+  piped_processt solver_process;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

From 829c778ff6c1d94afc54d222342d4221574e5542 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:14 +0100
Subject: [PATCH 02/18] Update existing test to add correct z3 arguments

So that the z3 sub process is actually started and expecting smt2
commands from the pipe in this test.
---
 .../incremental_solver_called.desc                            | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
index d79d1530ef8..be1e5f1bfa2 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
---incremental-smt2-solver z3
-Passing problem to incremental SMT2 solving via "z3"
+--incremental-smt2-solver "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
 identifier: main::1::x

From aad1bf526cedf26c277890274466d828f7e91829 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:15 +0100
Subject: [PATCH 03/18] Send initialisation commands to solver

---
 .../smt2_incremental/smt2_incremental_decision_procedure.cpp  | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 046aec27ce0..acfbe5c8042 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -2,6 +2,7 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
 #include <util/string_utils.h>
@@ -12,6 +13,9 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     number_of_solver_calls{0},
     solver_process{split_string(solver_command, ' ', false, true)}
 {
+  send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
+  send_to_solver(smt_set_logic_commandt{
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)

From 3e9b4a87a1b96beef62dbc6d6cdef64c17bd1183 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:16 +0100
Subject: [PATCH 04/18] Add debug logging of commands sent to SMT2 solver

So that we can see the text sent to the solver when debugging and so
that the text can be checked in regression tests. The commands are shown
as debug output messages rather than written to file because a file
based approach is not well suited to incremental solving.
---
 src/goto-checker/solver_factory.cpp                 |  2 +-
 .../smt2_incremental_decision_procedure.cpp         | 13 +++++++++----
 .../smt2_incremental_decision_procedure.h           | 13 ++++++++++---
 3 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index cd4136cfced..7799221aab2 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -333,7 +333,7 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      std::move(solver_command)));
+      std::move(solver_command), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index acfbe5c8042..4842f53be32 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -8,10 +8,12 @@
 #include <util/string_utils.h>
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
-  std::string _solver_command)
-  : solver_command{std::move(_solver_command)},
+  std::string _solver_command,
+  message_handlert &message_handler)
+  : solver_command(std::move(_solver_command)),
     number_of_solver_calls{0},
-    solver_process{split_string(solver_command, ' ', false, true)}
+    solver_process{split_string(solver_command, ' ', false, true)},
+    log{message_handler}
 {
   send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
   send_to_solver(smt_set_logic_commandt{
@@ -83,5 +85,8 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 void smt2_incremental_decision_proceduret::send_to_solver(
   const smt_commandt &command)
 {
-  solver_process.send(smt_to_smt2_string(command) + "\n");
+  const std::string command_string = smt_to_smt2_string(command);
+  log.debug() << "Sending command to SMT2 solver - " << command_string
+              << messaget::eom;
+  solver_process.send(command_string + "\n");
 }
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index 51504f623c8..9c0f6c0a568 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -7,17 +7,23 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
 #include <solvers/stack_decision_procedure.h>
+#include <util/message.h>
 #include <util/piped_process.h>
 
 class smt_commandt;
+class message_handlert;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
 {
 public:
-  /// \param solver_command: The command and arguments for invoking the smt2
-  ///                        solver.
-  explicit smt2_incremental_decision_proceduret(std::string solver_command);
+  /// \param solver_command:
+  ///   The command and arguments for invoking the smt2 solver.
+  /// \param message_handler:
+  ///   The messaging system to be used for logging purposes.
+  explicit smt2_incremental_decision_proceduret(
+    std::string solver_command,
+    message_handlert &message_handler);
 
   // Implementation of public decision_proceduret member functions.
   exprt handle(const exprt &expr) override;
@@ -44,6 +50,7 @@ class smt2_incremental_decision_proceduret final
   size_t number_of_solver_calls;
 
   piped_processt solver_process;
+  messaget log;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

From 778962e15d828e727d7e11adb43088facc6f571b Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:17 +0100
Subject: [PATCH 05/18] Add test of the setup commands sent to smt2 solver

---
 .../incremental_solver_called.desc                            | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
index be1e5f1bfa2..1122d9a1daa 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -1,7 +1,9 @@
 CORE
 test.c
---incremental-smt2-solver "z3 --smt2 -in"
+--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Sending command to SMT2 solver - \(set-option :produce-models true\)
+Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
 identifier: main::1::x

From 9027d981de639e7011e8338afbe9257df1361a9a Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:19 +0100
Subject: [PATCH 06/18] Implement symbol_exprt to smt_termt conversion

---
 src/solvers/smt2_incremental/convert_expr_to_smt.cpp  | 4 ++--
 unit/solvers/smt2_incremental/convert_expr_to_smt.cpp | 7 +++++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 5d753de7eeb..6d08eaf8c6a 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -46,8 +46,8 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
 
 static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for symbol expression: " + symbol_expr.pretty());
+  return smt_identifier_termt{symbol_expr.get_identifier(),
+                              convert_type_to_smt_sort(symbol_expr.type())};
 }
 
 static smt_termt convert_expr_to_smt(const nondet_symbol_exprt &nondet_symbol)
diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 6efa2440211..907583764c6 100644
--- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -34,6 +34,13 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
+{
+  CHECK(
+    convert_expr_to_smt(symbol_exprt{"foo", bool_typet{}}) ==
+    smt_identifier_termt("foo", smt_bool_sortt{}));
+}
+
 TEST_CASE(
   "\"exprt\" to smt term conversion for constants/literals",
   "[core][smt2_incremental]")

From fba062981635bb657b22faa20c02b14ca0f58b44 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:20 +0100
Subject: [PATCH 07/18] Add namespace access to
 `smt2_incremental_decision_proceduret`

So that instances of `symbol_exprt` can be handled correctly.
---
 src/goto-checker/solver_factory.cpp                         | 2 +-
 .../smt2_incremental_decision_procedure.cpp                 | 5 ++++-
 .../smt2_incremental/smt2_incremental_decision_procedure.h  | 6 ++++++
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index 7799221aab2..d5cfabac7d9 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -333,7 +333,7 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      std::move(solver_command), message_handler));
+      ns, std::move(solver_command), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 4842f53be32..034bb3a3b80 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -5,12 +5,15 @@
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
+#include <util/namespace.h>
 #include <util/string_utils.h>
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
+  const namespacet &_ns,
   std::string _solver_command,
   message_handlert &message_handler)
-  : solver_command(std::move(_solver_command)),
+  : ns{_ns},
+    solver_command(std::move(_solver_command)),
     number_of_solver_calls{0},
     solver_process{split_string(solver_command, ' ', false, true)},
     log{message_handler}
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index 9c0f6c0a568..d3b419963f2 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -12,16 +12,20 @@
 
 class smt_commandt;
 class message_handlert;
+class namespacet;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
 {
 public:
+  /// \param _ns: Namespace for looking up the expressions which symbol_exprts
+  ///   relate to.
   /// \param solver_command:
   ///   The command and arguments for invoking the smt2 solver.
   /// \param message_handler:
   ///   The messaging system to be used for logging purposes.
   explicit smt2_incremental_decision_proceduret(
+    const namespacet &_ns,
     std::string solver_command,
     message_handlert &message_handler);
 
@@ -45,6 +49,8 @@ class smt2_incremental_decision_proceduret final
   ///    solver process.
   void send_to_solver(const smt_commandt &command);
 
+  const namespacet &ns;
+
   /// This is where we store the solver command for reporting the solver used.
   std::string solver_command;
   size_t number_of_solver_calls;

From f286c07c07de31e0e0f335929b2c47adc6047a5b Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:21 +0100
Subject: [PATCH 08/18] Add conversion of exprs to SMT2 and sending to solver
 process

---
 .../incremental_solver_called.desc            |   6 +
 .../smt2_incremental_decision_procedure.cpp   | 120 +++++++++++++++++-
 .../smt2_incremental_decision_procedure.h     |  25 ++++
 3 files changed, 148 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
index 1122d9a1daa..029055b082b 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -4,6 +4,12 @@ test.c
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
+Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(assert |B2|\)
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
 identifier: main::1::x
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 034bb3a3b80..bc5a3f03bc3 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -2,11 +2,93 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#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_terms.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
 #include <util/namespace.h>
+#include <util/range.h>
+#include <util/std_expr.h>
 #include <util/string_utils.h>
+#include <util/symbol.h>
+
+#include <stack>
+
+/// \brief Find all sub expressions of the given \p expr which need to be
+///   expressed as separate smt commands.
+/// \note This pass over \p expr is tightly coupled to the implementation of
+///   `convert_expr_to_smt`. This is because any sub expressions which
+///   `convert_expr_to_smt` translates into function applications, must also be
+///   returned by this`gather_dependent_expressions` function.
+static std::unordered_set<exprt, irep_hash>
+gather_dependent_expressions(const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> dependent_expressions;
+  expr.visit_pre([&](const exprt &expr_node) {
+    if(can_cast_expr<symbol_exprt>(expr_node))
+    {
+      dependent_expressions.insert(expr_node);
+    }
+  });
+  return dependent_expressions;
+}
+
+/// \brief Defines any functions which \p expr depends on, which have not yet
+///   been defined, along with their dependencies in turn.
+void smt2_incremental_decision_proceduret::define_dependent_functions(
+  const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> seen_expressions =
+    make_range(expression_identifiers)
+      .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
+        return expr_identifier.first;
+      });
+  std::stack<exprt> to_be_defined;
+  const auto dependencies_needed = [&](const exprt &expr) {
+    bool result = false;
+    for(const auto &dependency : gather_dependent_expressions(expr))
+    {
+      if(!seen_expressions.insert(dependency).second)
+        continue;
+      result = true;
+      to_be_defined.push(dependency);
+    }
+    return result;
+  };
+  dependencies_needed(expr);
+  while(!to_be_defined.empty())
+  {
+    const exprt current = to_be_defined.top();
+    if(dependencies_needed(current))
+      continue;
+    if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
+    {
+      const irep_idt &identifier = symbol_expr->get_identifier();
+      const symbolt *symbol = nullptr;
+      if(!ns.lookup(identifier, symbol))
+      {
+        if(dependencies_needed(symbol->value))
+          continue;
+        const smt_define_function_commandt function{
+          symbol->name, {}, convert_expr_to_smt(symbol->value)};
+        expression_identifiers.emplace(*symbol_expr, function.identifier());
+        send_to_solver(function);
+      }
+      else
+      {
+        const smt_declare_function_commandt function{
+          smt_identifier_termt(
+            identifier, convert_type_to_smt_sort(symbol_expr->type())),
+          {}};
+        expression_identifiers.emplace(*symbol_expr, function.identifier());
+        send_to_solver(function);
+      }
+    }
+    to_be_defined.pop();
+  }
+}
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   const namespacet &_ns,
@@ -23,8 +105,27 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
+void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
+  const exprt &expr)
+{
+  if(
+    expression_handle_identifiers.find(expr) !=
+    expression_handle_identifiers.cend())
+  {
+    return;
+  }
+
+  define_dependent_functions(expr);
+  smt_define_function_commandt function{
+    "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
+  expression_handle_identifiers.emplace(expr, function.identifier());
+  send_to_solver(function);
+}
+
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
 {
+  log.debug() << "`handle`  -\n  " << expr.pretty(2, 0) << messaget::eom;
+  ensure_handle_for_expr_defined(expr);
   return expr;
 }
 
@@ -53,9 +154,22 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
 
 void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
 {
-  UNIMPLEMENTED_FEATURE(
-    "`set_to` (" + std::string{value ? "true" : "false"} + "):\n  " +
-    expr.pretty(2, 0));
+  PRECONDITION(can_cast_type<bool_typet>(expr.type()));
+  log.debug() << "`set_to` (" << std::string{value ? "true" : "false"}
+              << ") -\n  " << expr.pretty(2, 0) << messaget::eom;
+
+  define_dependent_functions(expr);
+  auto converted_term = [&]() -> smt_termt {
+    const auto expression_handle_identifier =
+      expression_handle_identifiers.find(expr);
+    if(expression_handle_identifier != expression_handle_identifiers.cend())
+      return expression_handle_identifier->second;
+    else
+      return convert_expr_to_smt(expr);
+  }();
+  if(!value)
+    converted_term = smt_core_theoryt::make_not(converted_term);
+  send_to_solver(smt_assert_commandt{converted_term});
 }
 
 void smt2_incremental_decision_proceduret::push(
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index d3b419963f2..dc2cc8f3e66 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -6,9 +6,14 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
+#include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/stack_decision_procedure.h>
 #include <util/message.h>
 #include <util/piped_process.h>
+#include <util/std_expr.h>
+
+#include <unordered_map>
+#include <unordered_set>
 
 class smt_commandt;
 class message_handlert;
@@ -48,6 +53,10 @@ class smt2_incremental_decision_proceduret final
   /// \brief Converts given SMT2 command to SMT2 string and sends it to the
   ///    solver process.
   void send_to_solver(const smt_commandt &command);
+  /// \brief Defines any functions which \p expr depends on, which have not yet
+  ///   been defined, along with their dependencies in turn.
+  void define_dependent_functions(const exprt &expr);
+  void ensure_handle_for_expr_defined(const exprt &expr);
 
   const namespacet &ns;
 
@@ -57,6 +66,22 @@ class smt2_incremental_decision_proceduret final
 
   piped_processt solver_process;
   messaget log;
+
+  class sequencet
+  {
+    size_t next_id = 0;
+
+  public:
+    size_t operator()()
+    {
+      return next_id++;
+    }
+  } handle_sequence;
+
+  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    expression_handle_identifiers;
+  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    expression_identifiers;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

From 6bc8b1f1633254aa5a0a7e95211a77521b867f66 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:22 +0100
Subject: [PATCH 09/18] Implement `dec_solve`

---
 .../incremental_solver_called.desc                  | 13 +++++++------
 .../smt2_incremental_decision_procedure.cpp         |  5 ++++-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
index 029055b082b..cd534e8198a 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -10,16 +10,17 @@ Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0
 Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
 Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(|not| false\)\)
 Sending command to SMT2 solver - \(assert |B2|\)
+Sending command to SMT2 solver - \(check-sat\)
+Solver response - sat
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
-identifier: main::1::x
 --
 type: pointer
 --
 Test that running cbmc with the `--incremental-smt2-solver` argument causes the
 incremental smt2 solving to be used. Note that at the time of adding this test,
-an invariant violation is expected due to the unimplemented solving.
-Regexes matching the printing in the expected failed invariant are included in
-order to test that `--slice-formula` is causing the first unimplemented
-expression passed to `smt2_incremental_decision_proceduret` to relate to the
-variable `x` in function `main` and not to `cprover_initialise`.
+an invariant violation is expected due to the unimplemented response parsing.
+
+The sliced formula is expected to use only the implemented subset of exprts.
+This is implementation is sufficient to send this example to the solver and
+receive a "sat" response.
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index bc5a3f03bc3..5964d350240 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -196,7 +196,10 @@ void smt2_incremental_decision_proceduret::pop()
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  UNIMPLEMENTED_FEATURE("solving.");
+  send_to_solver(smt_check_sat_commandt{});
+  const auto result = solver_process.wait_receive();
+  log.debug() << "Solver response - " << result << messaget::eom;
+  UNIMPLEMENTED_FEATURE("parsing of solver response.");
 }
 
 void smt2_incremental_decision_proceduret::send_to_solver(

From b6bfe4845b1040bb62e3dc77e9fa07ed96a50e88 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:23 +0100
Subject: [PATCH 10/18] Fix guard identifier processing

The identifier for guards includes the `\` character. Therefore this
commit is needed for allowing smt identifiers to be constructed
including this character and converted to string.
---
 src/solvers/smt2_incremental/smt_terms.cpp           |  4 ++--
 unit/solvers/smt2_incremental/smt_terms.cpp          |  2 +-
 unit/solvers/smt2_incremental/smt_to_smt2_string.cpp | 12 ++++++++++++
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp
index 72300fab67a..852748ce593 100644
--- a/src/solvers/smt2_incremental/smt_terms.cpp
+++ b/src/solvers/smt2_incremental/smt_terms.cpp
@@ -50,7 +50,7 @@ bool smt_bool_literal_termt::value() const
 
 static bool is_valid_smt_identifier(irep_idt identifier)
 {
-  static const std::regex valid{R"(^[^\|\\]*$)"};
+  static const std::regex valid{R"(^[^\|]*$)"};
   return std::regex_match(id2string(identifier), valid);
 }
 
@@ -59,7 +59,7 @@ smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
 {
   INVARIANT(
     is_valid_smt_identifier(identifier),
-    R"(Identifiers may not contain | or \ characters.)");
+    R"(Identifiers may not contain | characters.)");
   set(ID_identifier, identifier);
 }
 
diff --git a/unit/solvers/smt2_incremental/smt_terms.cpp b/unit/solvers/smt2_incremental/smt_terms.cpp
index 94f87b9e481..fdc873b40ad 100644
--- a/unit/solvers/smt2_incremental/smt_terms.cpp
+++ b/unit/solvers/smt2_incremental/smt_terms.cpp
@@ -39,7 +39,7 @@ TEST_CASE("smt_identifier_termt construction", "[core][smt2_incremental]")
   cbmc_invariants_should_throwt invariants_throw;
   CHECK_NOTHROW(smt_identifier_termt{"foo bar", smt_bool_sortt{}});
   CHECK_THROWS(smt_identifier_termt{"|foo bar|", smt_bool_sortt{}});
-  CHECK_THROWS(smt_identifier_termt{"foo\\ bar", smt_bool_sortt{}});
+  CHECK_NOTHROW(smt_identifier_termt{"foo\\ bar", smt_bool_sortt{}});
 }
 
 TEST_CASE("smt_identifier_termt getters.", "[core][smt2_incremental]")
diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
index 2ed9c9d86bc..ff158f92faf 100644
--- a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
+++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
@@ -32,6 +32,18 @@ TEST_CASE(
   CHECK(smt_to_smt2_string(smt_bool_literal_termt{false}) == "false");
 }
 
+TEST_CASE(
+  "Test smt_identifier_termt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) ==
+    "|abc|");
+  CHECK(
+    smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) ==
+    "|&92;|");
+}
+
 TEST_CASE(
   "Test smt_function_application_termt to string conversion",
   "[core][smt2_incremental]")

From 74a83f78041688fcdbe95f8cc2e90b03e00d5d9a Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 22 Sep 2021 10:34:24 +0100
Subject: [PATCH 11/18] Add test of an example with control flow

In order to check that guards are converted ok.
---
 .../control_flow.c                            | 16 ++++++++++
 .../control_flow.desc                         | 32 +++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.c
 create mode 100644 regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.c b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.c
new file mode 100644
index 00000000000..7a424b01c3c
--- /dev/null
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.c
@@ -0,0 +1,16 @@
+
+int main()
+{
+  int x, y;
+  if(x != 0)
+  {
+    y = 9;
+  }
+  else
+  {
+    y = 4;
+  }
+  int z = y;
+  __CPROVER_assert(x != z, "Assert of integer equality.");
+  return 0;
+}
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
new file mode 100644
index 00000000000..1472db4e382
--- /dev/null
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
@@ -0,0 +1,32 @@
+CORE
+control_flow.c
+--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Sending command to SMT2 solver - \(set-option :produce-models true\)
+Sending command to SMT2 solver - \(set-logic QF_UFBV\)
+Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |goto_symex::&92;guard#1| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(declare-fun |main::1::y!0@1#4| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |main::1::y!0@1#4| \(|ite| |goto_symex::&92;guard#1| \(_ bv9 32\) \(_ bv4 32\)\)\)\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#3| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |main::1::x!0@1#3| \(|ite| |goto_symex::&92;guard#1| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)
+Sending command to SMT2 solver - \(declare-fun |main::1::z!0@1#2| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(assert \(|=| |main::1::z!0@1#2| |main::1::y!0@1#4|\)\)
+Sending command to SMT2 solver - \(define-fun |B3| \(\) Bool \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)
+Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#3| |main::1::z!0@1#2|\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B4| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(assert |B4|\)
+Sending command to SMT2 solver - \(check-sat\)
+Solver response - sat
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--
+type: pointer
+--
+Test that running cbmc with the `--incremental-smt2-solver` argument can be used
+to send a valid SMT2 formula to a sub-process solver for an example input file
+which include control flow constructs. Note that at the time of adding this
+test, an invariant violation is expected due to the unimplemented response
+parsing.

From 5f01e32d629ac1f113705c8cfc513aebbba9ed53 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Mon, 27 Sep 2021 15:58:11 +0100
Subject: [PATCH 12/18] Disable running incremental smt2 tests on Windows

These tests currently fail when run on Windows due to issues with
`piped_processt`. This commit can be reverted once the debugging is
complete.
---
 regression/cbmc-incr-smt2/CMakeLists.txt                  | 8 +++++++-
 regression/cbmc-incr-smt2/Makefile                        | 8 +++++++-
 .../nondeterministic-int-assert/control_flow.desc         | 2 +-
 .../incremental_solver_called.desc                        | 2 +-
 4 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt
index dbdc826c667..06a41cf3496 100644
--- a/regression/cbmc-incr-smt2/CMakeLists.txt
+++ b/regression/cbmc-incr-smt2/CMakeLists.txt
@@ -1,4 +1,10 @@
 
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+    set(exclude_win_broken_tests -X winbug)
+else()
+    set(exclude_win_broken_tests "")
+endif()
+
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
 )
diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile
index 8bf6a9e88a6..603200de746 100644
--- a/regression/cbmc-incr-smt2/Makefile
+++ b/regression/cbmc-incr-smt2/Makefile
@@ -3,8 +3,14 @@ default: test
 include ../../src/config.inc
 include ../../src/common
 
+ifeq ($(BUILD_ENV_),MSVC)
+	exclude_broken_windows_tests=-X winbug
+else
+	exclude_broken_windows_tests=
+endif
+
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
 
 tests.log: ../test.pl test
 
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
index 1472db4e382..7209ee2712e 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 control_flow.c
 --incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
index cd534e8198a..5c962f022ac 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 test.c
 --incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"

From 3bc5ee4756b87915ba62bc5c6cbe5b5327f16440 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 28 Sep 2021 19:58:13 +0100
Subject: [PATCH 13/18] Refactor to separate solver communication from decision
 process

So that `smt2_incremental_decision_proceduret` can be unit tested in
isolation using a mock smt solver process.
---
 src/goto-checker/solver_factory.cpp           |  5 +-
 src/solvers/Makefile                          |  1 +
 .../smt2_incremental_decision_procedure.cpp   | 38 +++++--------
 .../smt2_incremental_decision_procedure.h     | 16 ++----
 src/solvers/smt2_incremental/smt_responses.h  | 21 +++++++
 .../smt2_incremental/smt_solver_process.cpp   | 36 ++++++++++++
 .../smt2_incremental/smt_solver_process.h     | 56 +++++++++++++++++++
 7 files changed, 138 insertions(+), 35 deletions(-)
 create mode 100644 src/solvers/smt2_incremental/smt_responses.h
 create mode 100644 src/solvers/smt2_incremental/smt_solver_process.cpp
 create mode 100644 src/solvers/smt2_incremental/smt_solver_process.h

diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index d5cfabac7d9..77a18d124dc 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -33,6 +33,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/sat/external_sat.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
+#include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/strings/string_refinement.h>
 
 solver_factoryt::solver_factoryt(
@@ -330,10 +331,12 @@ std::unique_ptr<solver_factoryt::solvert>
 solver_factoryt::get_incremental_smt2(std::string solver_command)
 {
   no_beautification();
+  auto solver_process = util_make_unique<smt_piped_solver_processt>(
+    std::move(solver_command), message_handler);
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      ns, std::move(solver_command), message_handler));
+      ns, std::move(solver_process), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index bcabc12fdfc..d854ece26fe 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -199,6 +199,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_core_theory.cpp \
       smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_options.cpp \
+      smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 5964d350240..6bea9728ecd 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -5,8 +5,8 @@
 #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_solver_process.h>
 #include <solvers/smt2_incremental/smt_terms.h>
-#include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/range.h>
@@ -74,7 +74,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         const smt_define_function_commandt function{
           symbol->name, {}, convert_expr_to_smt(symbol->value)};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
-        send_to_solver(function);
+        solver_process->send(function);
       }
       else
       {
@@ -83,7 +83,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
             identifier, convert_type_to_smt_sort(symbol_expr->type())),
           {}};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
-        send_to_solver(function);
+        solver_process->send(function);
       }
     }
     to_be_defined.pop();
@@ -92,16 +92,16 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   const namespacet &_ns,
-  std::string _solver_command,
+  std::unique_ptr<smt_base_solver_processt> _solver_process,
   message_handlert &message_handler)
   : ns{_ns},
-    solver_command(std::move(_solver_command)),
     number_of_solver_calls{0},
-    solver_process{split_string(solver_command, ' ', false, true)},
+    solver_process(std::move(_solver_process)),
     log{message_handler}
 {
-  send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
-  send_to_solver(smt_set_logic_commandt{
+  solver_process->send(
+    smt_set_option_commandt{smt_option_produce_modelst{true}});
+  solver_process->send(smt_set_logic_commandt{
     smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
@@ -119,7 +119,7 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   smt_define_function_commandt function{
     "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
   expression_handle_identifiers.emplace(expr, function.identifier());
-  send_to_solver(function);
+  solver_process->send(function);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -143,7 +143,7 @@ void smt2_incremental_decision_proceduret::print_assignment(
 std::string
 smt2_incremental_decision_proceduret::decision_procedure_text() const
 {
-  return "incremental SMT2 solving via \"" + solver_command + "\"";
+  return "incremental SMT2 solving via " + solver_process->description();
 }
 
 std::size_t
@@ -169,7 +169,7 @@ void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
   }();
   if(!value)
     converted_term = smt_core_theoryt::make_not(converted_term);
-  send_to_solver(smt_assert_commandt{converted_term});
+  solver_process->send(smt_assert_commandt{converted_term});
 }
 
 void smt2_incremental_decision_proceduret::push(
@@ -196,17 +196,7 @@ void smt2_incremental_decision_proceduret::pop()
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  send_to_solver(smt_check_sat_commandt{});
-  const auto result = solver_process.wait_receive();
-  log.debug() << "Solver response - " << result << messaget::eom;
-  UNIMPLEMENTED_FEATURE("parsing of solver response.");
-}
-
-void smt2_incremental_decision_proceduret::send_to_solver(
-  const smt_commandt &command)
-{
-  const std::string command_string = smt_to_smt2_string(command);
-  log.debug() << "Sending command to SMT2 solver - " << command_string
-              << messaget::eom;
-  solver_process.send(command_string + "\n");
+  solver_process->send(smt_check_sat_commandt{});
+  const smt_responset result = solver_process->receive_response();
+  UNIMPLEMENTED_FEATURE("handling solver response.");
 }
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index dc2cc8f3e66..7d84ad8707d 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -9,15 +9,16 @@
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/stack_decision_procedure.h>
 #include <util/message.h>
-#include <util/piped_process.h>
 #include <util/std_expr.h>
 
+#include <memory>
 #include <unordered_map>
 #include <unordered_set>
 
 class smt_commandt;
 class message_handlert;
 class namespacet;
+class smt_base_solver_processt;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
@@ -25,13 +26,13 @@ class smt2_incremental_decision_proceduret final
 public:
   /// \param _ns: Namespace for looking up the expressions which symbol_exprts
   ///   relate to.
-  /// \param solver_command:
-  ///   The command and arguments for invoking the smt2 solver.
+  /// \param solver_process:
+  ///   The smt2 solver process communication interface.
   /// \param message_handler:
   ///   The messaging system to be used for logging purposes.
   explicit smt2_incremental_decision_proceduret(
     const namespacet &_ns,
-    std::string solver_command,
+    std::unique_ptr<smt_base_solver_processt> solver_process,
     message_handlert &message_handler);
 
   // Implementation of public decision_proceduret member functions.
@@ -50,9 +51,6 @@ class smt2_incremental_decision_proceduret final
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
-  /// \brief Converts given SMT2 command to SMT2 string and sends it to the
-  ///    solver process.
-  void send_to_solver(const smt_commandt &command);
   /// \brief Defines any functions which \p expr depends on, which have not yet
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);
@@ -60,11 +58,9 @@ class smt2_incremental_decision_proceduret final
 
   const namespacet &ns;
 
-  /// This is where we store the solver command for reporting the solver used.
-  std::string solver_command;
   size_t number_of_solver_calls;
 
-  piped_processt solver_process;
+  std::unique_ptr<smt_base_solver_processt> solver_process;
   messaget log;
 
   class sequencet
diff --git a/src/solvers/smt2_incremental/smt_responses.h b/src/solvers/smt2_incremental/smt_responses.h
new file mode 100644
index 00000000000..d93a0b59652
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_responses.h
@@ -0,0 +1,21 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
+
+#include <util/irep.h>
+
+class smt_responset : protected irept
+{
+public:
+  // smt_responset does not support the notion of an empty / null state. Use
+  // optionalt<smt_responset> instead if an empty response is required.
+  smt_responset() = delete;
+
+  using irept::pretty;
+
+protected:
+  using irept::irept;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
diff --git a/src/solvers/smt2_incremental/smt_solver_process.cpp b/src/solvers/smt2_incremental/smt_solver_process.cpp
new file mode 100644
index 00000000000..148aefbf259
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_solver_process.cpp
@@ -0,0 +1,36 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_solver_process.h>
+
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <util/invariant.h>
+#include <util/string_utils.h>
+
+smt_piped_solver_processt::smt_piped_solver_processt(
+  std::string command_line,
+  message_handlert &message_handler)
+  : command_line_description{"\"" + command_line + "\""},
+    process{split_string(command_line, ' ', false, true)},
+    log{message_handler}
+{
+}
+
+const std::string &smt_piped_solver_processt::description()
+{
+  return command_line_description;
+}
+
+void smt_piped_solver_processt::send(const smt_commandt &smt_command)
+{
+  const std::string command_string = smt_to_smt2_string(smt_command);
+  log.debug() << "Sending command to SMT2 solver - " << command_string
+              << messaget::eom;
+  process.send(command_string + "\n");
+}
+
+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.");
+}
diff --git a/src/solvers/smt2_incremental/smt_solver_process.h b/src/solvers/smt2_incremental/smt_solver_process.h
new file mode 100644
index 00000000000..de094f13b01
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_solver_process.h
@@ -0,0 +1,56 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
+
+class smt_commandt;
+
+#include <solvers/smt2_incremental/smt_responses.h>
+#include <util/message.h>
+#include <util/piped_process.h>
+
+#include <string>
+
+class smt_base_solver_processt
+{
+public:
+  virtual const std::string &description() = 0;
+
+  /// \brief Converts given SMT2 command to SMT2 string and sends it to the
+  ///    solver process.
+  virtual void send(const smt_commandt &command) = 0;
+
+  virtual smt_responset receive_response() = 0;
+
+  virtual ~smt_base_solver_processt() = default;
+};
+
+class smt_piped_solver_processt : public smt_base_solver_processt
+{
+public:
+  /// \param command_line:
+  ///   The command and arguments for invoking the smt2 solver.
+  /// \param message_handler:
+  ///   The messaging system to be used for logging purposes.
+  smt_piped_solver_processt(
+    std::string command_line,
+    message_handlert &message_handler);
+
+  const std::string &description() override;
+
+  void send(const smt_commandt &smt_command) override;
+
+  smt_responset receive_response() override;
+
+  ~smt_piped_solver_processt() override = default;
+
+protected:
+  /// The command line used to start the process.
+  std::string command_line_description;
+  /// The raw solver sub process.
+  piped_processt process;
+  /// For debug printing.
+  messaget log;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H

From 6c33e07817aac4da249e6c5b84e54f6aa6a62039 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 30 Sep 2021 15:42:40 +0100
Subject: [PATCH 14/18] Fix handling of symbols with no value

Because there was previously an assumption that all symbols in the
symbol table had values and it is more straight forward to make the this
code deal with that than to add an invariant.
---
 .../smt2_incremental/smt2_incremental_decision_procedure.cpp    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 6bea9728ecd..03d20c477e7 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -67,7 +67,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
     {
       const irep_idt &identifier = symbol_expr->get_identifier();
       const symbolt *symbol = nullptr;
-      if(!ns.lookup(identifier, symbol))
+      if(!ns.lookup(identifier, symbol) && !symbol->value.is_nil())
       {
         if(dependencies_needed(symbol->value))
           continue;

From 28759bc1d6581dadb6f8c629eeaa68de5cd1a4c9 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 30 Sep 2021 15:49:41 +0100
Subject: [PATCH 15/18] Refactor symbol lookup

The previous implementation contained 2x "not" operations. By appling De
Morgan's laws these operations can be dispensed with and the code is
thus made more readable.
---
 .../smt2_incremental_decision_procedure.cpp    | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 03d20c477e7..ec2ff4ba34e 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -67,21 +67,21 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
     {
       const irep_idt &identifier = symbol_expr->get_identifier();
       const symbolt *symbol = nullptr;
-      if(!ns.lookup(identifier, symbol) && !symbol->value.is_nil())
+      if(ns.lookup(identifier, symbol) || symbol->value.is_nil())
       {
-        if(dependencies_needed(symbol->value))
-          continue;
-        const smt_define_function_commandt function{
-          symbol->name, {}, convert_expr_to_smt(symbol->value)};
+        const smt_declare_function_commandt function{
+          smt_identifier_termt(
+            identifier, convert_type_to_smt_sort(symbol_expr->type())),
+          {}};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
         solver_process->send(function);
       }
       else
       {
-        const smt_declare_function_commandt function{
-          smt_identifier_termt(
-            identifier, convert_type_to_smt_sort(symbol_expr->type())),
-          {}};
+        if(dependencies_needed(symbol->value))
+          continue;
+        const smt_define_function_commandt function{
+          symbol->name, {}, convert_expr_to_smt(symbol->value)};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
         solver_process->send(function);
       }

From 91da8ba507af6d0e3068bf1b4ebe99c19c7d00fb Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 28 Sep 2021 21:09:17 +0100
Subject: [PATCH 16/18] Add smt2_incremental_decision_proceduret unit tests

---
 unit/Makefile                                 |   1 +
 .../smt2_incremental_decision_procedure.cpp   | 206 ++++++++++++++++++
 2 files changed, 207 insertions(+)
 create mode 100644 unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

diff --git a/unit/Makefile b/unit/Makefile
index 730050466b4..6627c489b8f 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -99,6 +99,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/smt2/smt2_conv.cpp \
        solvers/smt2_incremental/convert_expr_to_smt.cpp \
+       solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
        solvers/smt2_incremental/smt_core_theory.cpp \
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
new file mode 100644
index 00000000000..8b5451bec76
--- /dev/null
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -0,0 +1,206 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#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_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/make_unique.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+class smt_mock_solver_processt : public smt_base_solver_processt
+{
+public:
+  const std::string &description() override
+  {
+    UNREACHABLE;
+  }
+
+  void send(const smt_commandt &smt_command) override
+  {
+    sent_commands.push_back(smt_command);
+  }
+
+  smt_responset receive_response() override
+  {
+    UNREACHABLE;
+  }
+
+  std::vector<smt_commandt> sent_commands;
+
+  ~smt_mock_solver_processt() override = default;
+};
+
+static symbolt make_test_symbol(irep_idt id, typet type)
+{
+  symbolt new_symbol;
+  new_symbol.name = std::move(id);
+  new_symbol.type = std::move(type);
+  return new_symbol;
+}
+
+static symbolt make_test_symbol(irep_idt id, exprt value)
+{
+  symbolt new_symbol;
+  new_symbol.name = std::move(id);
+  new_symbol.type = value.type();
+  new_symbol.value = std::move(value);
+  return new_symbol;
+}
+
+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;
+  SECTION("Construction / solver initialisation.")
+  {
+    smt2_incremental_decision_proceduret procedure{
+      ns, std::move(mock_process), message_handler};
+    REQUIRE(
+      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();
+    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);
+      REQUIRE(
+        sent_commands ==
+        std::vector<smt_commandt>{smt_declare_function_commandt{foo_term, {}},
+                                  smt_assert_commandt{foo_term}});
+    }
+    SECTION("Set symbol to false.")
+    {
+      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);
+      REQUIRE(
+        sent_commands ==
+        std::vector<smt_commandt>{
+          smt_declare_function_commandt{foo_term, {}},
+          smt_assert_commandt{smt_core_theoryt::make_not(foo_term)}});
+    }
+    SECTION("Set using chaining of symbol expressions.")
+    {
+      const symbolt forty_two =
+        make_test_symbol("forty_two", from_integer({42}, signedbv_typet{16}));
+      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);
+      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);
+      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);
+      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);
+      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);
+      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);
+      smt_identifier_termt comparison_conjunction_term{"comparison_conjunction",
+                                                       smt_bool_sortt{}};
+      procedure.set_to(comparison_conjunction.symbol_expr(), true);
+      REQUIRE(
+        sent_commands ==
+        std::vector<smt_commandt>{
+          smt_declare_function_commandt{nondet_int_b_term, {}},
+          smt_declare_function_commandt{nondet_int_a_term, {}},
+          smt_define_function_commandt{
+            "third_comparison",
+            {},
+            smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
+          smt_define_function_commandt{
+            "forty_two", {}, smt_bit_vector_constant_termt{42, 16}},
+          smt_define_function_commandt{
+            "second_comparison",
+            {},
+            smt_core_theoryt::make_not(
+              smt_core_theoryt::equal(nondet_int_b_term, forty_two_term))},
+          smt_define_function_commandt{
+            "first_comparison",
+            {},
+            smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
+          smt_define_function_commandt{
+            "comparison_conjunction",
+            {},
+            smt_core_theoryt::make_and(
+              smt_core_theoryt::make_and(
+                smt_identifier_termt{"first_comparison", smt_bool_sortt{}},
+                smt_identifier_termt{"second_comparison", smt_bool_sortt{}}),
+              smt_identifier_termt{"third_comparison", smt_bool_sortt{}})},
+          smt_assert_commandt{comparison_conjunction_term}});
+    }
+    SECTION("Handle of value-less symbol.")
+    {
+      const symbolt foo = make_test_symbol("foo", bool_typet{});
+      const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
+      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();
+      SECTION("Handle of previously handled expression.")
+      {
+        procedure.handle(foo.symbol_expr());
+        REQUIRE(sent_commands.empty());
+      }
+      SECTION("Handle of new expression containing previously defined symbol.")
+      {
+        procedure.handle(equal_exprt{foo.symbol_expr(), foo.symbol_expr()});
+        REQUIRE(
+          sent_commands ==
+          std::vector<smt_commandt>{smt_define_function_commandt{
+            "B1", {}, smt_core_theoryt::equal(foo_term, foo_term)}});
+      }
+    }
+    SECTION("Handle of symbol with value.")
+    {
+      const symbolt bar =
+        make_test_symbol("bar", from_integer({42}, signedbv_typet{8}));
+      symbol_table.insert(bar);
+      procedure.handle(bar.symbol_expr());
+      REQUIRE(
+        sent_commands ==
+        std::vector<smt_commandt>{
+          smt_define_function_commandt{
+            "bar", {}, smt_bit_vector_constant_termt{42, 8}},
+          smt_define_function_commandt{
+            "B0", {}, smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}}});
+    }
+  }
+}

From 7a0da55b3f3faa664997f7e5f314b739a520331e Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 1 Oct 2021 11:40:04 +0100
Subject: [PATCH 17/18] Improve error printing in smt2 decision procedure unit
 test

In order to improve the chances of being able to see what is wrong
when/if the tests fail.
---
 .../smt2_incremental_decision_procedure.cpp                 | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 8b5451bec76..46f4f907538 100644
--- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -14,6 +14,12 @@
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
+// Used by catch framework for printing in the case of test failures. This
+// means that we get error messages showing the smt formula expressed as SMT2
+// strings instead of `{?}` being printed. It works because catch uses the
+// appropriate overload of `operator<<` where it exists.
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+
 class smt_mock_solver_processt : public smt_base_solver_processt
 {
 public:

From 71d746a0092024d9a176db096ce086657aca9873 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 1 Oct 2021 16:27:56 +0100
Subject: [PATCH 18/18] Make the order of SMT commands for sub-expressions
 deterministic

This makes the behaviour of the conversion predictable. This has the
advantage of being easier to unit test and reducing the possiblity of
hard to re-produce bugs.
---
 .../smt2_incremental_decision_procedure.cpp        | 11 +++++++----
 .../smt2_incremental_decision_procedure.cpp        | 14 +++++++-------
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index ec2ff4ba34e..0d6661de16f 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -18,18 +18,21 @@
 
 /// \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
+///   separate smt commands. This collection is in traversal order. It will
+///   include duplicate subexpressions, which need to be removed by the caller
+///   in order to avoid duplicate definitions.
 /// \note This pass over \p expr is tightly coupled to the implementation of
 ///   `convert_expr_to_smt`. This is because any sub expressions which
 ///   `convert_expr_to_smt` translates into function applications, must also be
 ///   returned by this`gather_dependent_expressions` function.
-static std::unordered_set<exprt, irep_hash>
-gather_dependent_expressions(const exprt &expr)
+static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
 {
-  std::unordered_set<exprt, irep_hash> dependent_expressions;
+  std::vector<exprt> dependent_expressions;
   expr.visit_pre([&](const exprt &expr_node) {
     if(can_cast_expr<symbol_exprt>(expr_node))
     {
-      dependent_expressions.insert(expr_node);
+      dependent_expressions.push_back(expr_node);
     }
   });
   return dependent_expressions;
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 46f4f907538..13444d7b121 100644
--- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -143,23 +143,23 @@ TEST_CASE(
       REQUIRE(
         sent_commands ==
         std::vector<smt_commandt>{
-          smt_declare_function_commandt{nondet_int_b_term, {}},
           smt_declare_function_commandt{nondet_int_a_term, {}},
-          smt_define_function_commandt{
-            "third_comparison",
-            {},
-            smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
           smt_define_function_commandt{
             "forty_two", {}, smt_bit_vector_constant_termt{42, 16}},
+          smt_define_function_commandt{
+            "first_comparison",
+            {},
+            smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
+          smt_declare_function_commandt{nondet_int_b_term, {}},
           smt_define_function_commandt{
             "second_comparison",
             {},
             smt_core_theoryt::make_not(
               smt_core_theoryt::equal(nondet_int_b_term, forty_two_term))},
           smt_define_function_commandt{
-            "first_comparison",
+            "third_comparison",
             {},
-            smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
+            smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
           smt_define_function_commandt{
             "comparison_conjunction",
             {},