From 5558cee47e5311ad5c27f8db9856537b56503a70 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 20 Jul 2021 19:52:28 +0100
Subject: [PATCH 1/9] Add check on the number of bits in bit vector sorts

Because the bit vector theory defined in SMT2 does not allow for bit
vectors of 0 bits.
---
 src/solvers/smt2_incremental/smt_sorts.cpp  | 4 ++++
 unit/solvers/smt2_incremental/smt_sorts.cpp | 8 ++++++++
 2 files changed, 12 insertions(+)

diff --git a/src/solvers/smt2_incremental/smt_sorts.cpp b/src/solvers/smt2_incremental/smt_sorts.cpp
index bc721afd061..8a2567731f8 100644
--- a/src/solvers/smt2_incremental/smt_sorts.cpp
+++ b/src/solvers/smt2_incremental/smt_sorts.cpp
@@ -27,6 +27,10 @@ smt_bool_sortt::smt_bool_sortt() : smt_sortt{ID_smt_bool_sort}
 smt_bit_vector_sortt::smt_bit_vector_sortt(const std::size_t bit_width)
   : smt_sortt{ID_smt_bit_vector_sort}
 {
+  INVARIANT(
+    bit_width > 0,
+    "The definition of SMT2 bit vector theory requires the number of "
+    "bits to be greater than 0.");
   set_size_t(ID_width, bit_width);
 }
 
diff --git a/unit/solvers/smt2_incremental/smt_sorts.cpp b/unit/solvers/smt2_incremental/smt_sorts.cpp
index 94f532d3ece..50c1e3ec7fb 100644
--- a/unit/solvers/smt2_incremental/smt_sorts.cpp
+++ b/unit/solvers/smt2_incremental/smt_sorts.cpp
@@ -10,6 +10,14 @@ TEST_CASE("Test smt_sortt.pretty is accessible.", "[core][smt2_incremental]")
   REQUIRE(bool_sort.pretty(0, 0) == "smt_bool_sort");
 }
 
+TEST_CASE(
+  "Test smt_bit_vec_sortt bit width invariant",
+  "[core][smt2_incremental]")
+{
+  const cbmc_invariants_should_throwt invariants_throw_during_test;
+  REQUIRE_THROWS(smt_bit_vector_sortt{0});
+}
+
 TEST_CASE(
   "Test smt_bit_vec_sortt bit_width getter.",
   "[core][smt2_incremental]")

From 9f256caaaa03890f2996945d6f5ca00e19f987cc Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 16 Jun 2021 10:16:41 +0100
Subject: [PATCH 2/9] Add conversion of `smt_sortt` into strings

So that they can be sent to an SMT2 solver using a string based
interface.
---
 src/solvers/Makefile                          |  1 +
 .../smt2_incremental/smt_to_string.cpp        | 43 +++++++++++++++++++
 src/solvers/smt2_incremental/smt_to_string.h  | 18 ++++++++
 unit/Makefile                                 |  1 +
 .../smt2_incremental/smt_to_string.cpp        | 12 ++++++
 5 files changed, 75 insertions(+)
 create mode 100644 src/solvers/smt2_incremental/smt_to_string.cpp
 create mode 100644 src/solvers/smt2_incremental/smt_to_string.h
 create mode 100644 unit/solvers/smt2_incremental/smt_to_string.cpp

diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 4b02b0621ff..d82e4a1b3b3 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -197,6 +197,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
+      smt2_incremental/smt_to_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       # Empty last line
 
diff --git a/src/solvers/smt2_incremental/smt_to_string.cpp b/src/solvers/smt2_incremental/smt_to_string.cpp
new file mode 100644
index 00000000000..67b3ce5d67a
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_to_string.cpp
@@ -0,0 +1,43 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_to_string.h>
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
+{
+protected:
+  std::ostream &os;
+
+public:
+  explicit smt_sort_output_visitort(std::ostream &os) : os(os)
+  {
+  }
+
+  void visit(const smt_bool_sortt &) override
+  {
+    os << "Bool";
+  }
+
+  void visit(const smt_bit_vector_sortt &bit_vec) override
+  {
+    os << "(_ BitVec " << bit_vec.bit_width() << ")";
+  }
+};
+
+std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
+{
+  sort.accept(smt_sort_output_visitort{os});
+  return os;
+}
+
+std::string smt_to_string(const smt_sortt &sort)
+{
+  std::stringstream ss;
+  ss << sort;
+  return ss.str();
+}
diff --git a/src/solvers/smt2_incremental/smt_to_string.h b/src/solvers/smt2_incremental/smt_to_string.h
new file mode 100644
index 00000000000..3565e39b253
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_to_string.h
@@ -0,0 +1,18 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Streaming SMT data structures to a string based output stream.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
+
+class smt_sortt;
+
+#include <iosfwd>
+#include <string>
+
+std::ostream &operator<<(std::ostream &os, const smt_sortt &sort);
+
+std::string smt_to_string(const smt_sortt &sort);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
diff --git a/unit/Makefile b/unit/Makefile
index 46fab54b042..b13ccc96f20 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -88,6 +88,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
        solvers/smt2_incremental/smt_sorts.cpp \
        solvers/smt2_incremental/smt_terms.cpp \
+       solvers/smt2_incremental/smt_to_string.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
diff --git a/unit/solvers/smt2_incremental/smt_to_string.cpp b/unit/solvers/smt2_incremental/smt_to_string.cpp
new file mode 100644
index 00000000000..17c0b14c520
--- /dev/null
+++ b/unit/solvers/smt2_incremental/smt_to_string.cpp
@@ -0,0 +1,12 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+#include <solvers/smt2_incremental/smt_to_string.h>
+
+TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_bool_sortt{}) == "Bool");
+  CHECK(smt_to_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
+}

From 7ca5546a0e29d3d71faa26a0beca026632c24dd4 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Mon, 12 Jul 2021 17:35:32 +0100
Subject: [PATCH 3/9] Add conversion of `smt_termt` to strings

So that they can be sent to an SMT2 solver using a string based
interface.
---
 .../smt2_incremental/smt_to_string.cpp        | 188 ++++++++++++++++++
 src/solvers/smt2_incremental/smt_to_string.h  |   3 +
 .../smt2_incremental/smt_to_string.cpp        |  37 ++++
 3 files changed, 228 insertions(+)

diff --git a/src/solvers/smt2_incremental/smt_to_string.cpp b/src/solvers/smt2_incremental/smt_to_string.cpp
index 67b3ce5d67a..dedecf3b86d 100644
--- a/src/solvers/smt2_incremental/smt_to_string.cpp
+++ b/src/solvers/smt2_incremental/smt_to_string.cpp
@@ -2,10 +2,16 @@
 
 #include <solvers/smt2_incremental/smt_to_string.h>
 
+#include <solvers/smt2/smt2_conv.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
+#include <solvers/smt2_incremental/smt_terms.h>
 
+#include <util/range.h>
+
+#include <functional>
 #include <iostream>
 #include <sstream>
+#include <stack>
 #include <string>
 
 class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
@@ -41,3 +47,185 @@ std::string smt_to_string(const smt_sortt &sort)
   ss << sort;
   return ss.str();
 }
+
+/// \note The printing algorithm in the `smt_term_to_string_convertert` class is
+///   implemented using an explicit `std::stack` rather than using recursion
+///   and the call stack. This is done in order to ensure we can print smt terms
+///   which are nested arbitrarily deeply without risk of exceeding the maximum
+///   depth of the call stack.
+/// \details
+///   The set of `visit` functions push functions to `output_stack`,
+///   which capture the value to be printed. When called these functions may
+///   either print to the output stream or push further functions to the stack
+///   in the case of nodes in the tree which have child nodes which also need to
+///   be printed.
+///   The `push_output(s)` functions exist as convenience functions to allow
+///   pushing the capturing functions to the stack in the reverse order required
+///   for printing, whilst keeping the visit functions easier to read by keeping
+///   the outputs in reading order and separating the capturing code.
+class smt_term_to_string_convertert : private smt_term_const_downcast_visitort
+{
+private:
+  using output_functiont = std::function<void(std::ostream &)>;
+  std::stack<output_functiont> output_stack;
+
+  static output_functiont make_output_function(const std::string &output);
+  static output_functiont make_output_function(const smt_sortt &output);
+  output_functiont make_output_function(const smt_termt &output);
+  output_functiont make_output_function(
+    const std::vector<std::reference_wrapper<const smt_termt>> &output);
+
+  /// \brief Single argument version of `push_outputs`.
+  template <typename outputt>
+  void push_output(outputt &&output);
+
+  /// \brief Base case for the recursive `push_outputs` function template below.
+  void push_outputs();
+
+  /// \brief Pushes outputting functions to the output_stack for each of the
+  ///   output values provided. This variadic template supports any (compile
+  ///   time fixed) number of output arguments.
+  /// \details The arguments are pushed in order from right to left, so that
+  ///   they are subsequently in left to right order when popped off the stack.
+  ///   The types of argument supported are those supported by the overloads of
+  ///   the `make_output_function` function.
+  /// \note This is implemented recursively, but does not risk exceeding the
+  ///   maximum depth of the call stack. This is because the number of times it
+  ///   recurses depends only on the number of arguments supplied in the source
+  ///   code at compile time.
+  template <typename outputt, typename... outputst>
+  void push_outputs(outputt &&output, outputst &&... outputs);
+
+  smt_term_to_string_convertert() = default;
+
+  void visit(const smt_bool_literal_termt &bool_literal) override;
+  void visit(const smt_not_termt &not_term) override;
+  void visit(const smt_identifier_termt &identifier_term) override;
+  void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override;
+  void
+  visit(const smt_function_application_termt &function_application) override;
+
+public:
+  /// \brief This function is complete the external interface to this class. All
+  ///   construction of this class and printing of terms should be carried out
+  ///   via this function.
+  static std::ostream &convert(std::ostream &os, const smt_termt &term);
+};
+
+smt_term_to_string_convertert::output_functiont
+smt_term_to_string_convertert::make_output_function(const std::string &output)
+{
+  // `output` must be captured by value to avoid dangling references.
+  return [output](std::ostream &os) { os << output; };
+}
+
+smt_term_to_string_convertert::output_functiont
+smt_term_to_string_convertert::make_output_function(const smt_sortt &output)
+{
+  // `output` can be safely captured by reference, because no sorts are copied
+  // or constructed as part of conversion to string.
+  return [&](std::ostream &os) { os << output; };
+}
+
+smt_term_to_string_convertert::output_functiont
+smt_term_to_string_convertert::make_output_function(const smt_termt &output)
+{
+  // `output` can be safely captured by reference, because no terms are copied
+  // or constructed as part of conversion to string.
+  return [&](std::ostream &os) { output.accept(*this); };
+}
+
+smt_term_to_string_convertert::output_functiont
+smt_term_to_string_convertert::make_output_function(
+  const std::vector<std::reference_wrapper<const smt_termt>> &outputs)
+{
+  // `outputs` must be captured by value to avoid a dangling reference to the
+  // vector. The elements in the vector are not at risk of dangling as the
+  // lifetime of the terms to which they refer is at least as long as the
+  // execution of the overall printing algorithm.
+  return [&, outputs](std::ostream &os) {
+    for(const auto &output : make_range(outputs.rbegin(), outputs.rend()))
+    {
+      push_outputs(" ", output.get());
+    }
+  };
+}
+
+template <typename outputt>
+void smt_term_to_string_convertert::push_output(outputt &&output)
+{
+  output_stack.push(make_output_function(std::forward<outputt>(output)));
+}
+
+void smt_term_to_string_convertert::push_outputs()
+{
+}
+
+template <typename outputt, typename... outputst>
+void smt_term_to_string_convertert::push_outputs(
+  outputt &&output,
+  outputst &&... outputs)
+{
+  push_outputs(std::forward<outputst>(outputs)...);
+  push_output(std::forward<outputt>(output));
+}
+
+void smt_term_to_string_convertert::visit(
+  const smt_bool_literal_termt &bool_literal)
+{
+  push_output(bool_literal.value() ? "true" : "false");
+}
+
+void smt_term_to_string_convertert::visit(const smt_not_termt &not_term)
+{
+  push_outputs("(not ", not_term.operand(), ")");
+}
+
+void smt_term_to_string_convertert::visit(
+  const smt_identifier_termt &identifier_term)
+{
+  push_outputs(
+    "|", smt2_convt::convert_identifier(identifier_term.identifier()), "|");
+}
+
+void smt_term_to_string_convertert::visit(
+  const smt_bit_vector_constant_termt &bit_vector_constant)
+{
+  auto value = integer2string(bit_vector_constant.value());
+  auto bit_width = std::to_string(bit_vector_constant.get_sort().bit_width());
+  push_outputs("(_ bv", std::move(value), " ", std::move(bit_width), ")");
+}
+
+void smt_term_to_string_convertert::visit(
+  const smt_function_application_termt &function_application)
+{
+  const auto &id = function_application.function_identifier();
+  auto arguments = function_application.arguments();
+  push_outputs("(", id, std::move(arguments), ")");
+}
+
+std::ostream &
+smt_term_to_string_convertert::convert(std::ostream &os, const smt_termt &term)
+{
+  smt_term_to_string_convertert converter;
+  term.accept(converter);
+  while(!converter.output_stack.empty())
+  {
+    auto output_function = std::move(converter.output_stack.top());
+    converter.output_stack.pop();
+    output_function(os);
+  }
+  return os;
+}
+
+std::ostream &operator<<(std::ostream &os, const smt_termt &term)
+{
+  return smt_term_to_string_convertert::convert(os, term);
+}
+
+std::string smt_to_string(const smt_termt &term)
+{
+  std::stringstream ss;
+  ss << term;
+  return ss.str();
+}
diff --git a/src/solvers/smt2_incremental/smt_to_string.h b/src/solvers/smt2_incremental/smt_to_string.h
index 3565e39b253..b2680fa140d 100644
--- a/src/solvers/smt2_incremental/smt_to_string.h
+++ b/src/solvers/smt2_incremental/smt_to_string.h
@@ -7,12 +7,15 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
 
 class smt_sortt;
+class smt_termt;
 
 #include <iosfwd>
 #include <string>
 
 std::ostream &operator<<(std::ostream &os, const smt_sortt &sort);
+std::ostream &operator<<(std::ostream &os, const smt_termt &term);
 
 std::string smt_to_string(const smt_sortt &sort);
+std::string smt_to_string(const smt_termt &term);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
diff --git a/unit/solvers/smt2_incremental/smt_to_string.cpp b/unit/solvers/smt2_incremental/smt_to_string.cpp
index 17c0b14c520..948400de1c4 100644
--- a/unit/solvers/smt2_incremental/smt_to_string.cpp
+++ b/unit/solvers/smt2_incremental/smt_to_string.cpp
@@ -3,10 +3,47 @@
 #include <testing-utils/use_catch.h>
 
 #include <solvers/smt2_incremental/smt_sorts.h>
+#include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/smt2_incremental/smt_to_string.h>
 
+#include <util/mp_arith.h>
+
 TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
 {
   CHECK(smt_to_string(smt_bool_sortt{}) == "Bool");
   CHECK(smt_to_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
 }
+
+TEST_CASE("Test smt_not_termt to string conversion", "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_string(smt_not_termt{
+      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(not |foo|)");
+}
+
+TEST_CASE(
+  "Test smt_bit_vector_constant_termt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_bit_vector_constant_termt{0, 8}) == "(_ bv0 8)");
+}
+
+TEST_CASE(
+  "Test smt_bool_literal_termt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_bool_literal_termt{true}) == "true");
+  CHECK(smt_to_string(smt_bool_literal_termt{false}) == "false");
+}
+
+TEST_CASE(
+  "Test smt_function_application_termt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_string(smt_function_application_termt{
+      smt_identifier_termt{"=", smt_bool_sortt{}},
+      {smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
+       {smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}}}}) ==
+    "(|=| |foo| |bar|)");
+}

From 27cba980b807d6c4a718ba44fb1c7585231ed9d9 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 20 Jul 2021 20:00:13 +0100
Subject: [PATCH 4/9] Make identifier of define function command an
 identifier_term

For uniformity with `smt_declare_function_commandt` and ease of
correctly escaping the identifer when converting to string.
---
 src/solvers/smt2_incremental/smt_commands.cpp  | 9 ++++++---
 src/solvers/smt2_incremental/smt_commands.h    | 2 +-
 unit/solvers/smt2_incremental/smt_commands.cpp | 4 +++-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt_commands.cpp b/src/solvers/smt2_incremental/smt_commands.cpp
index 45bfc418e38..6df79441599 100644
--- a/src/solvers/smt2_incremental/smt_commands.cpp
+++ b/src/solvers/smt2_incremental/smt_commands.cpp
@@ -83,7 +83,9 @@ smt_define_function_commandt::smt_define_function_commandt(
   smt_termt definition)
   : smt_commandt{ID_smt_define_function_command}
 {
-  set(ID_identifier, identifier);
+  set(
+    ID_identifier,
+    upcast(smt_identifier_termt{std::move(identifier), definition.get_sort()}));
   std::transform(
     std::make_move_iterator(parameters.begin()),
     std::make_move_iterator(parameters.end()),
@@ -94,9 +96,10 @@ smt_define_function_commandt::smt_define_function_commandt(
   set(ID_code, upcast(std::move(definition)));
 }
 
-const irep_idt &smt_define_function_commandt::identifier() const
+const smt_identifier_termt &smt_define_function_commandt::identifier() const
 {
-  return get(ID_identifier);
+  return static_cast<const smt_identifier_termt &>(
+    downcast(find(ID_identifier)));
 }
 
 std::vector<std::reference_wrapper<const smt_identifier_termt>>
diff --git a/src/solvers/smt2_incremental/smt_commands.h b/src/solvers/smt2_incremental/smt_commands.h
index 2b06f5b9fa5..aece515e41a 100644
--- a/src/solvers/smt2_incremental/smt_commands.h
+++ b/src/solvers/smt2_incremental/smt_commands.h
@@ -70,7 +70,7 @@ class smt_define_function_commandt
     irep_idt identifier,
     std::vector<smt_identifier_termt> parameters,
     smt_termt definition);
-  const irep_idt &identifier() const;
+  const smt_identifier_termt &identifier() const;
   std::vector<std::reference_wrapper<const smt_identifier_termt>>
   parameters() const;
   const smt_sortt &return_sort() const;
diff --git a/unit/solvers/smt2_incremental/smt_commands.cpp b/unit/solvers/smt2_incremental/smt_commands.cpp
index 8aefb52a1f9..510574d7fae 100644
--- a/unit/solvers/smt2_incremental/smt_commands.cpp
+++ b/unit/solvers/smt2_incremental/smt_commands.cpp
@@ -37,7 +37,9 @@ TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]")
     {smt_identifier_termt{"x", smt_bool_sortt{}},
      smt_identifier_termt{"y", smt_bool_sortt{}}},
     smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}}};
-  CHECK(function_definition.identifier() == "not first");
+  CHECK(
+    function_definition.identifier() ==
+    smt_identifier_termt{"not first", smt_bool_sortt{}});
   CHECK(
     function_definition.parameters()[0].get() ==
     smt_identifier_termt{"x", smt_bool_sortt{}});

From 47032156d61daf377c8f670f29a4e4c42a104865 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 7 Jul 2021 17:49:58 +0100
Subject: [PATCH 5/9] Add conversion of `smt_commandt` to strings

So that they can be sent to an SMT2 solver using a string based
interface.
---
 .../smt2_incremental/smt_to_string.cpp        | 152 ++++++++++++++++++
 src/solvers/smt2_incremental/smt_to_string.h  |   9 ++
 .../smt2_incremental/smt_to_string.cpp        |  94 +++++++++++
 3 files changed, 255 insertions(+)

diff --git a/src/solvers/smt2_incremental/smt_to_string.cpp b/src/solvers/smt2_incremental/smt_to_string.cpp
index dedecf3b86d..e5635ecb29b 100644
--- a/src/solvers/smt2_incremental/smt_to_string.cpp
+++ b/src/solvers/smt2_incremental/smt_to_string.cpp
@@ -3,10 +3,13 @@
 #include <solvers/smt2_incremental/smt_to_string.h>
 
 #include <solvers/smt2/smt2_conv.h>
+#include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_logics.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 
 #include <util/range.h>
+#include <util/string_utils.h>
 
 #include <functional>
 #include <iostream>
@@ -229,3 +232,152 @@ std::string smt_to_string(const smt_termt &term)
   ss << term;
   return ss.str();
 }
+
+class smt_option_to_string_convertert
+  : public smt_option_const_downcast_visitort
+{
+protected:
+  std::ostream &os;
+
+public:
+  explicit smt_option_to_string_convertert(std::ostream &os) : os(os)
+  {
+  }
+
+  void visit(const smt_option_produce_modelst &produce_models) override
+  {
+    os << ":produce-models " << (produce_models.setting() ? "true" : "false");
+  }
+};
+
+std::ostream &operator<<(std::ostream &os, const smt_optiont &option)
+{
+  option.accept(smt_option_to_string_convertert{os});
+  return os;
+}
+
+std::string smt_to_string(const smt_optiont &option)
+{
+  std::stringstream ss;
+  ss << option;
+  return ss.str();
+}
+
+class smt_logic_to_string_convertert : public smt_logic_const_downcast_visitort
+{
+protected:
+  std::ostream &os;
+
+public:
+  explicit smt_logic_to_string_convertert(std::ostream &os) : os(os)
+  {
+  }
+
+  void visit(const smt_logic_quantifier_free_bit_vectorst &) override
+  {
+    os << "QF_BV";
+  }
+};
+
+std::ostream &operator<<(std::ostream &os, const smt_logict &logic)
+{
+  logic.accept(smt_logic_to_string_convertert{os});
+  return os;
+}
+
+std::string smt_to_string(const smt_logict &logic)
+{
+  std::stringstream ss;
+  ss << logic;
+  return ss.str();
+}
+
+class smt_command_to_string_convertert
+  : public smt_command_const_downcast_visitort
+{
+protected:
+  std::ostream &os;
+
+public:
+  explicit smt_command_to_string_convertert(std::ostream &os) : os(os)
+  {
+  }
+
+  void visit(const smt_assert_commandt &assert) override
+  {
+    os << "(assert " << assert.condition() << ")";
+  }
+
+  void visit(const smt_check_sat_commandt &check_sat) override
+  {
+    os << "(check-sat)";
+  }
+
+  void visit(const smt_declare_function_commandt &declare_function) override
+  {
+    os << "(declare-fun " << declare_function.identifier() << " (";
+    const auto parameter_sorts = declare_function.parameter_sorts();
+    join_strings(os, parameter_sorts.begin(), parameter_sorts.end(), ' ');
+    os << ") " << declare_function.return_sort() << ")";
+  }
+
+  void visit(const smt_define_function_commandt &define_function) override
+  {
+    os << "(define-fun " << define_function.identifier() << " (";
+    const auto parameters = define_function.parameters();
+    join_strings(
+      os,
+      parameters.begin(),
+      parameters.end(),
+      " ",
+      [](const smt_identifier_termt &identifier) {
+        return "(" + smt_to_string(identifier) + " " +
+               smt_to_string(identifier.get_sort()) + ")";
+      });
+    os << ") " << define_function.return_sort() << " "
+       << define_function.definition() << ")";
+  }
+
+  void visit(const smt_exit_commandt &exit) override
+  {
+    os << "(exit)";
+  }
+
+  void visit(const smt_get_value_commandt &get_value) override
+  {
+    os << "(get-value " << get_value.descriptor() << ")";
+  }
+
+  void visit(const smt_pop_commandt &pop) override
+  {
+    os << "(pop " << pop.levels() << ")";
+  }
+
+  void visit(const smt_push_commandt &push) override
+  {
+    os << "(push " << push.levels() << ")";
+  }
+
+  void visit(const smt_set_logic_commandt &set_logic) override
+  {
+    os << "(set-logic " << set_logic.logic() << ")";
+  }
+
+  void visit(const smt_set_option_commandt &set_option) override
+  {
+    os << "(set-option " << set_option.option() << ")";
+  }
+};
+
+std::ostream &operator<<(std::ostream &os, const smt_commandt &command)
+{
+  command.accept(smt_command_to_string_convertert{os});
+  return os;
+}
+
+std::string smt_to_string(const smt_commandt &command)
+{
+  std::stringstream ss;
+  ss << command;
+  return ss.str();
+}
diff --git a/src/solvers/smt2_incremental/smt_to_string.h b/src/solvers/smt2_incremental/smt_to_string.h
index b2680fa140d..1d00886ec4a 100644
--- a/src/solvers/smt2_incremental/smt_to_string.h
+++ b/src/solvers/smt2_incremental/smt_to_string.h
@@ -8,14 +8,23 @@
 
 class smt_sortt;
 class smt_termt;
+class smt_optiont;
+class smt_commandt;
+class smt_logict;
 
 #include <iosfwd>
 #include <string>
 
 std::ostream &operator<<(std::ostream &os, const smt_sortt &sort);
 std::ostream &operator<<(std::ostream &os, const smt_termt &term);
+std::ostream &operator<<(std::ostream &os, const smt_optiont &option);
+std::ostream &operator<<(std::ostream &os, const smt_logict &logic);
+std::ostream &operator<<(std::ostream &os, const smt_commandt &command);
 
 std::string smt_to_string(const smt_sortt &sort);
 std::string smt_to_string(const smt_termt &term);
+std::string smt_to_string(const smt_optiont &option);
+std::string smt_to_string(const smt_logict &logic);
+std::string smt_to_string(const smt_commandt &command);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
diff --git a/unit/solvers/smt2_incremental/smt_to_string.cpp b/unit/solvers/smt2_incremental/smt_to_string.cpp
index 948400de1c4..ddcd287af3b 100644
--- a/unit/solvers/smt2_incremental/smt_to_string.cpp
+++ b/unit/solvers/smt2_incremental/smt_to_string.cpp
@@ -2,6 +2,8 @@
 
 #include <testing-utils/use_catch.h>
 
+#include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_logics.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/smt2_incremental/smt_to_string.h>
@@ -47,3 +49,95 @@ TEST_CASE(
        {smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}}}}) ==
     "(|=| |foo| |bar|)");
 }
+
+TEST_CASE(
+  "Test smt_check_sat_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_check_sat_commandt{}) == "(check-sat)");
+}
+
+TEST_CASE(
+  "Test smt_exit_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_exit_commandt{}) == "(exit)");
+}
+
+TEST_CASE(
+  "Test smt_push_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_push_commandt{1}) == "(push 1)");
+  CHECK(smt_to_string(smt_push_commandt{2}) == "(push 2)");
+}
+
+TEST_CASE(
+  "Test smt_pop_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_pop_commandt{1}) == "(pop 1)");
+  CHECK(smt_to_string(smt_pop_commandt{2}) == "(pop 2)");
+}
+
+TEST_CASE(
+  "Test smt_assert_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_string(smt_assert_commandt{smt_bool_literal_termt{true}}) ==
+    "(assert true)");
+}
+
+TEST_CASE(
+  "Test smt_declare_function_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_string(smt_declare_function_commandt{
+      smt_identifier_termt{"f", smt_bit_vector_sortt{31}},
+      {smt_bit_vector_sortt{32}, smt_bit_vector_sortt{33}}}) ==
+    "(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))");
+}
+
+TEST_CASE(
+  "Test smt_define_function_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  const auto g = smt_identifier_termt{"g", smt_bit_vector_sortt{32}};
+  const auto h = smt_identifier_termt{"h", smt_bit_vector_sortt{32}};
+
+  CHECK(
+    smt_to_string(smt_define_function_commandt{
+      "f",
+      {g, h},
+      smt_function_application_termt{
+        smt_identifier_termt{"=", smt_bool_sortt{}}, {g, h}}}) ==
+    "(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| "
+    "|h|))");
+}
+
+TEST_CASE(
+  "Test smt_set_option_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  const auto with_models = smt_option_produce_modelst{true};
+  const auto no_models = smt_option_produce_modelst{false};
+  CHECK(smt_to_string(with_models) == ":produce-models true");
+  CHECK(smt_to_string(no_models) == ":produce-models false");
+  CHECK(
+    smt_to_string(smt_set_option_commandt{with_models}) ==
+    "(set-option :produce-models true)");
+  CHECK(
+    smt_to_string(smt_set_option_commandt{no_models}) ==
+    "(set-option :produce-models false)");
+}
+
+TEST_CASE(
+  "Test smt_set_logic_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  const smt_logic_quantifier_free_bit_vectorst qf_bv;
+  CHECK(smt_to_string(qf_bv) == "QF_BV");
+  CHECK(smt_to_string(smt_set_logic_commandt{qf_bv}) == "(set-logic QF_BV)");
+}

From aacc171c7562879d9a843f8bf0399990ecf50d5a Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 22 Jul 2021 14:31:58 +0100
Subject: [PATCH 6/9] Use capture by value in term to string conversion

Some of the outputs can currently be safely captured by value. However
there is the potential for accidentally introducing dangling reference
type bugs from changes elsewhere in the term to string conversion code.
Therefore this change will reduce the likelyhood of bugs being
introduced in future and should have minimal performance impact due to
the copy-on-write properties of ireps.
---
 src/solvers/smt2_incremental/smt_to_string.cpp | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt_to_string.cpp b/src/solvers/smt2_incremental/smt_to_string.cpp
index e5635ecb29b..63d7d88729c 100644
--- a/src/solvers/smt2_incremental/smt_to_string.cpp
+++ b/src/solvers/smt2_incremental/smt_to_string.cpp
@@ -125,28 +125,20 @@ smt_term_to_string_convertert::make_output_function(const std::string &output)
 smt_term_to_string_convertert::output_functiont
 smt_term_to_string_convertert::make_output_function(const smt_sortt &output)
 {
-  // `output` can be safely captured by reference, because no sorts are copied
-  // or constructed as part of conversion to string.
-  return [&](std::ostream &os) { os << output; };
+  return [=](std::ostream &os) { os << output; };
 }
 
 smt_term_to_string_convertert::output_functiont
 smt_term_to_string_convertert::make_output_function(const smt_termt &output)
 {
-  // `output` can be safely captured by reference, because no terms are copied
-  // or constructed as part of conversion to string.
-  return [&](std::ostream &os) { output.accept(*this); };
+  return [=](std::ostream &os) { output.accept(*this); };
 }
 
 smt_term_to_string_convertert::output_functiont
 smt_term_to_string_convertert::make_output_function(
   const std::vector<std::reference_wrapper<const smt_termt>> &outputs)
 {
-  // `outputs` must be captured by value to avoid a dangling reference to the
-  // vector. The elements in the vector are not at risk of dangling as the
-  // lifetime of the terms to which they refer is at least as long as the
-  // execution of the overall printing algorithm.
-  return [&, outputs](std::ostream &os) {
+  return [=](std::ostream &os) {
     for(const auto &output : make_range(outputs.rbegin(), outputs.rend()))
     {
       push_outputs(" ", output.get());

From 14bfc682925ac99febc96d87727d80b6d2d6313a Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 23 Jul 2021 11:49:47 +0100
Subject: [PATCH 7/9] Rename `smt_to_string` as `smt_to_smt2_string`

In order to make the kind of string being converted to clearer.
---
 .../smt2_incremental/smt_to_string.cpp        | 14 +++---
 src/solvers/smt2_incremental/smt_to_string.h  | 10 ++---
 .../smt2_incremental/smt_to_string.cpp        | 45 ++++++++++---------
 3 files changed, 35 insertions(+), 34 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt_to_string.cpp b/src/solvers/smt2_incremental/smt_to_string.cpp
index 63d7d88729c..89dd5d1c7ef 100644
--- a/src/solvers/smt2_incremental/smt_to_string.cpp
+++ b/src/solvers/smt2_incremental/smt_to_string.cpp
@@ -44,7 +44,7 @@ std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
   return os;
 }
 
-std::string smt_to_string(const smt_sortt &sort)
+std::string smt_to_smt2_string(const smt_sortt &sort)
 {
   std::stringstream ss;
   ss << sort;
@@ -218,7 +218,7 @@ std::ostream &operator<<(std::ostream &os, const smt_termt &term)
   return smt_term_to_string_convertert::convert(os, term);
 }
 
-std::string smt_to_string(const smt_termt &term)
+std::string smt_to_smt2_string(const smt_termt &term)
 {
   std::stringstream ss;
   ss << term;
@@ -248,7 +248,7 @@ std::ostream &operator<<(std::ostream &os, const smt_optiont &option)
   return os;
 }
 
-std::string smt_to_string(const smt_optiont &option)
+std::string smt_to_smt2_string(const smt_optiont &option)
 {
   std::stringstream ss;
   ss << option;
@@ -277,7 +277,7 @@ std::ostream &operator<<(std::ostream &os, const smt_logict &logic)
   return os;
 }
 
-std::string smt_to_string(const smt_logict &logic)
+std::string smt_to_smt2_string(const smt_logict &logic)
 {
   std::stringstream ss;
   ss << logic;
@@ -323,8 +323,8 @@ class smt_command_to_string_convertert
       parameters.end(),
       " ",
       [](const smt_identifier_termt &identifier) {
-        return "(" + smt_to_string(identifier) + " " +
-               smt_to_string(identifier.get_sort()) + ")";
+        return "(" + smt_to_smt2_string(identifier) + " " +
+               smt_to_smt2_string(identifier.get_sort()) + ")";
       });
     os << ") " << define_function.return_sort() << " "
        << define_function.definition() << ")";
@@ -367,7 +367,7 @@ std::ostream &operator<<(std::ostream &os, const smt_commandt &command)
   return os;
 }
 
-std::string smt_to_string(const smt_commandt &command)
+std::string smt_to_smt2_string(const smt_commandt &command)
 {
   std::stringstream ss;
   ss << command;
diff --git a/src/solvers/smt2_incremental/smt_to_string.h b/src/solvers/smt2_incremental/smt_to_string.h
index 1d00886ec4a..45132e93a16 100644
--- a/src/solvers/smt2_incremental/smt_to_string.h
+++ b/src/solvers/smt2_incremental/smt_to_string.h
@@ -21,10 +21,10 @@ std::ostream &operator<<(std::ostream &os, const smt_optiont &option);
 std::ostream &operator<<(std::ostream &os, const smt_logict &logic);
 std::ostream &operator<<(std::ostream &os, const smt_commandt &command);
 
-std::string smt_to_string(const smt_sortt &sort);
-std::string smt_to_string(const smt_termt &term);
-std::string smt_to_string(const smt_optiont &option);
-std::string smt_to_string(const smt_logict &logic);
-std::string smt_to_string(const smt_commandt &command);
+std::string smt_to_smt2_string(const smt_sortt &sort);
+std::string smt_to_smt2_string(const smt_termt &term);
+std::string smt_to_smt2_string(const smt_optiont &option);
+std::string smt_to_smt2_string(const smt_logict &logic);
+std::string smt_to_smt2_string(const smt_commandt &command);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
diff --git a/unit/solvers/smt2_incremental/smt_to_string.cpp b/unit/solvers/smt2_incremental/smt_to_string.cpp
index ddcd287af3b..a2b1b35849a 100644
--- a/unit/solvers/smt2_incremental/smt_to_string.cpp
+++ b/unit/solvers/smt2_incremental/smt_to_string.cpp
@@ -12,14 +12,14 @@
 
 TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_bool_sortt{}) == "Bool");
-  CHECK(smt_to_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
+  CHECK(smt_to_smt2_string(smt_bool_sortt{}) == "Bool");
+  CHECK(smt_to_smt2_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
 }
 
 TEST_CASE("Test smt_not_termt to string conversion", "[core][smt2_incremental]")
 {
   CHECK(
-    smt_to_string(smt_not_termt{
+    smt_to_smt2_string(smt_not_termt{
       smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(not |foo|)");
 }
 
@@ -27,15 +27,15 @@ TEST_CASE(
   "Test smt_bit_vector_constant_termt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_bit_vector_constant_termt{0, 8}) == "(_ bv0 8)");
+  CHECK(smt_to_smt2_string(smt_bit_vector_constant_termt{0, 8}) == "(_ bv0 8)");
 }
 
 TEST_CASE(
   "Test smt_bool_literal_termt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_bool_literal_termt{true}) == "true");
-  CHECK(smt_to_string(smt_bool_literal_termt{false}) == "false");
+  CHECK(smt_to_smt2_string(smt_bool_literal_termt{true}) == "true");
+  CHECK(smt_to_smt2_string(smt_bool_literal_termt{false}) == "false");
 }
 
 TEST_CASE(
@@ -43,7 +43,7 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   CHECK(
-    smt_to_string(smt_function_application_termt{
+    smt_to_smt2_string(smt_function_application_termt{
       smt_identifier_termt{"=", smt_bool_sortt{}},
       {smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
        {smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}}}}) ==
@@ -54,30 +54,30 @@ TEST_CASE(
   "Test smt_check_sat_commandt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_check_sat_commandt{}) == "(check-sat)");
+  CHECK(smt_to_smt2_string(smt_check_sat_commandt{}) == "(check-sat)");
 }
 
 TEST_CASE(
   "Test smt_exit_commandt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_exit_commandt{}) == "(exit)");
+  CHECK(smt_to_smt2_string(smt_exit_commandt{}) == "(exit)");
 }
 
 TEST_CASE(
   "Test smt_push_commandt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_push_commandt{1}) == "(push 1)");
-  CHECK(smt_to_string(smt_push_commandt{2}) == "(push 2)");
+  CHECK(smt_to_smt2_string(smt_push_commandt{1}) == "(push 1)");
+  CHECK(smt_to_smt2_string(smt_push_commandt{2}) == "(push 2)");
 }
 
 TEST_CASE(
   "Test smt_pop_commandt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(smt_to_string(smt_pop_commandt{1}) == "(pop 1)");
-  CHECK(smt_to_string(smt_pop_commandt{2}) == "(pop 2)");
+  CHECK(smt_to_smt2_string(smt_pop_commandt{1}) == "(pop 1)");
+  CHECK(smt_to_smt2_string(smt_pop_commandt{2}) == "(pop 2)");
 }
 
 TEST_CASE(
@@ -85,7 +85,7 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   CHECK(
-    smt_to_string(smt_assert_commandt{smt_bool_literal_termt{true}}) ==
+    smt_to_smt2_string(smt_assert_commandt{smt_bool_literal_termt{true}}) ==
     "(assert true)");
 }
 
@@ -94,7 +94,7 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   CHECK(
-    smt_to_string(smt_declare_function_commandt{
+    smt_to_smt2_string(smt_declare_function_commandt{
       smt_identifier_termt{"f", smt_bit_vector_sortt{31}},
       {smt_bit_vector_sortt{32}, smt_bit_vector_sortt{33}}}) ==
     "(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))");
@@ -108,7 +108,7 @@ TEST_CASE(
   const auto h = smt_identifier_termt{"h", smt_bit_vector_sortt{32}};
 
   CHECK(
-    smt_to_string(smt_define_function_commandt{
+    smt_to_smt2_string(smt_define_function_commandt{
       "f",
       {g, h},
       smt_function_application_termt{
@@ -123,13 +123,13 @@ TEST_CASE(
 {
   const auto with_models = smt_option_produce_modelst{true};
   const auto no_models = smt_option_produce_modelst{false};
-  CHECK(smt_to_string(with_models) == ":produce-models true");
-  CHECK(smt_to_string(no_models) == ":produce-models false");
+  CHECK(smt_to_smt2_string(with_models) == ":produce-models true");
+  CHECK(smt_to_smt2_string(no_models) == ":produce-models false");
   CHECK(
-    smt_to_string(smt_set_option_commandt{with_models}) ==
+    smt_to_smt2_string(smt_set_option_commandt{with_models}) ==
     "(set-option :produce-models true)");
   CHECK(
-    smt_to_string(smt_set_option_commandt{no_models}) ==
+    smt_to_smt2_string(smt_set_option_commandt{no_models}) ==
     "(set-option :produce-models false)");
 }
 
@@ -138,6 +138,7 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   const smt_logic_quantifier_free_bit_vectorst qf_bv;
-  CHECK(smt_to_string(qf_bv) == "QF_BV");
-  CHECK(smt_to_string(smt_set_logic_commandt{qf_bv}) == "(set-logic QF_BV)");
+  CHECK(smt_to_smt2_string(qf_bv) == "QF_BV");
+  CHECK(
+    smt_to_smt2_string(smt_set_logic_commandt{qf_bv}) == "(set-logic QF_BV)");
 }

From 9eee2a7a518c01c81cb381f432e66c2efe83a69f Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 23 Jul 2021 12:14:36 +0100
Subject: [PATCH 8/9] Rename files from `smt_to_string` to `smt_to_smt2_string`

In order to make the kind of string being converted to clearer.
---
 src/solvers/Makefile                                        | 2 +-
 .../{smt_to_string.cpp => smt_to_smt2_string.cpp}           | 2 +-
 .../{smt_to_string.h => smt_to_smt2_string.h}               | 6 +++---
 unit/Makefile                                               | 2 +-
 .../{smt_to_string.cpp => smt_to_smt2_string.cpp}           | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)
 rename src/solvers/smt2_incremental/{smt_to_string.cpp => smt_to_smt2_string.cpp} (99%)
 rename src/solvers/smt2_incremental/{smt_to_string.h => smt_to_smt2_string.h} (82%)
 rename unit/solvers/smt2_incremental/{smt_to_string.cpp => smt_to_smt2_string.cpp} (98%)

diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index d82e4a1b3b3..6b6edee3a4e 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -197,7 +197,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
-      smt2_incremental/smt_to_string.cpp \
+      smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       # Empty last line
 
diff --git a/src/solvers/smt2_incremental/smt_to_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
similarity index 99%
rename from src/solvers/smt2_incremental/smt_to_string.cpp
rename to src/solvers/smt2_incremental/smt_to_smt2_string.cpp
index 89dd5d1c7ef..f4e4c48cf6b 100644
--- a/src/solvers/smt2_incremental/smt_to_string.cpp
+++ b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
@@ -1,6 +1,6 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/smt_to_string.h>
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
 
 #include <solvers/smt2/smt2_conv.h>
 #include <solvers/smt2_incremental/smt_commands.h>
diff --git a/src/solvers/smt2_incremental/smt_to_string.h b/src/solvers/smt2_incremental/smt_to_smt2_string.h
similarity index 82%
rename from src/solvers/smt2_incremental/smt_to_string.h
rename to src/solvers/smt2_incremental/smt_to_smt2_string.h
index 45132e93a16..52daacadd80 100644
--- a/src/solvers/smt2_incremental/smt_to_string.h
+++ b/src/solvers/smt2_incremental/smt_to_smt2_string.h
@@ -3,8 +3,8 @@
 /// \file
 /// Streaming SMT data structures to a string based output stream.
 
-#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
-#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H
 
 class smt_sortt;
 class smt_termt;
@@ -27,4 +27,4 @@ std::string smt_to_smt2_string(const smt_optiont &option);
 std::string smt_to_smt2_string(const smt_logict &logic);
 std::string smt_to_smt2_string(const smt_commandt &command);
 
-#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H
diff --git a/unit/Makefile b/unit/Makefile
index b13ccc96f20..1026b8bba0b 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -88,7 +88,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
        solvers/smt2_incremental/smt_sorts.cpp \
        solvers/smt2_incremental/smt_terms.cpp \
-       solvers/smt2_incremental/smt_to_string.cpp \
+       solvers/smt2_incremental/smt_to_smt2_string.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
diff --git a/unit/solvers/smt2_incremental/smt_to_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
similarity index 98%
rename from unit/solvers/smt2_incremental/smt_to_string.cpp
rename to unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
index a2b1b35849a..becdde33022 100644
--- a/unit/solvers/smt2_incremental/smt_to_string.cpp
+++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
@@ -6,7 +6,7 @@
 #include <solvers/smt2_incremental/smt_logics.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
-#include <solvers/smt2_incremental/smt_to_string.h>
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
 
 #include <util/mp_arith.h>
 

From 5dd2519aab1de7df40604ac90c18fa06106bcac7 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 23 Jul 2021 12:26:24 +0100
Subject: [PATCH 9/9] Extend doxygen to specify the targeted format standard

In order to be clear about the kind of strings which should be
generated.
---
 src/solvers/smt2_incremental/smt_to_smt2_string.h | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.h b/src/solvers/smt2_incremental/smt_to_smt2_string.h
index 52daacadd80..c8e78aa5255 100644
--- a/src/solvers/smt2_incremental/smt_to_smt2_string.h
+++ b/src/solvers/smt2_incremental/smt_to_smt2_string.h
@@ -1,7 +1,9 @@
 // Author: Diffblue Ltd.
 
 /// \file
-/// Streaming SMT data structures to a string based output stream.
+/// Streaming SMT data structures to a string based output stream. The generated
+/// output strings are intended to be valid input for SMT2 solvers compliant
+/// with the SMT-LIB standard version 2.6.
 
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H