diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 7a43c522d4e..4b02b0621ff 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -192,6 +192,11 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
+      smt2_incremental/smt_commands.cpp \
+      smt2_incremental/smt_logics.cpp \
+      smt2_incremental/smt_options.cpp \
+      smt2_incremental/smt_sorts.cpp \
+      smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       # Empty last line
 
diff --git a/src/solvers/smt2_incremental/internal_ast.txt b/src/solvers/smt2_incremental/internal_ast.txt
new file mode 100644
index 00000000000..0109a9d57d6
--- /dev/null
+++ b/src/solvers/smt2_incremental/internal_ast.txt
@@ -0,0 +1,255 @@
+@startuml
+' This diagram is written using PlantUML. It can be visualised locally or using
+' the PlantUML website - http://www.plantuml.com/plantuml/uml/.
+' On Linux the visualisation tool can be installed using -
+'   `sudo apt-get install plantuml`
+' Running the `plantuml` binary from the directory where this file exists will
+' give the option to view the file.
+
+title SMT2 Internal Abstract Syntax Tree Data Structures
+legend bottom right
+  Specification references refer to "The SMT-LIB Standard" Version 2.6
+endlegend
+
+class irept {
+	--
+	Protected inheritance to be used to prevent direct data access from outside
+	of the classes inheriting from it.
+	__
+}
+
+class smt_commandt {
+	..
+	Note - Protected constructor, so as to only allow construction as part of a
+	sub-class. Public copy/upcast/assignment to this class still available.
+	__
+}
+irept <|-- smt_commandt
+
+class smt_set_option_commandt {
+	""(set-option :produce-models true)""
+	--
+	Section 4.1.7 page 55
+	__
+	option : smt_optiont
+}
+smt_commandt <|-- smt_set_option_commandt
+smt_set_option_commandt *-- smt_optiont
+
+class smt_set_logic_commandt {
+	(set-logic QF_AUFBV)
+	--
+	__
+	logic : smt_logict
+}
+smt_commandt <|-- smt_set_logic_commandt
+smt_set_logic_commandt *-- smt_logict
+
+class smt_declare_function_commandt {
+	""(declare-fun |main::1::x!0@1#1| () (_ BitVec 32))""
+	--
+	Declares the sort (rank?) of a function, introducing the new identifier
+	""|main::1::x!0@1#1|"" in the above example.
+	__
+	identifier
+	parameter_sorts : std::vector<smt_sortt>
+	return_sort : smt_sortt
+}
+smt_commandt <|-- smt_declare_function_commandt
+smt_declare_function_commandt *-- smt_sortt
+
+class smt_define_function_commandt {
+	""(define-fun |B0| () Bool (= |main::1::x!0@1#1| |main::1::x!0@1#1|))""
+	--
+	Defines the implementation of a function. Note that the return_sort could be
+	stored in the "definition" term because all terms have a sort for our
+	definition of term.
+	__
+	identifier
+	parameters : std::vector<smt_identifier_termt>
+	return_sort : smt_sortt
+	definition : smt_termt
+}
+smt_commandt <|-- smt_define_function_commandt
+smt_define_function_commandt *-- smt_identifier_termt
+smt_define_function_commandt *-- smt_sortt
+smt_define_function_commandt *-- smt_termt
+
+class smt_assert_commandt {
+	""(assert |B1|)""
+	--
+	Note condition should be of sort ""smt_bool_sortt""
+	__
+	condition : smt_termt
+}
+smt_commandt <|-- smt_assert_commandt
+smt_assert_commandt *-- smt_termt
+
+class smt_check_sat_commandt {
+	""(check-sat)""
+	..
+	Section 4.2.5 page 64
+	__
+}
+smt_commandt <|-- smt_check_sat_commandt
+
+class smt_get_value_commandt {
+	""(get-value (|foo|))""
+	..
+	Section 4.2.6 page 65
+	Note: Identifier would usually be a smt_identifier_termt for our use case, but
+	the syntax allows more flexability than that.
+	__
+	identifier : smt_termt
+}
+smt_commandt <|-- smt_get_value_commandt
+smt_get_value_commandt *-- smt_termt
+
+class smt_exit_commandt {
+	""(exit)""
+	..
+	Section 4.2.1 page 59
+	Instructs the solver process to exit.
+	__
+}
+smt_commandt <|-- smt_exit_commandt
+
+class smt_pop_commandt {
+	""(pop 1)""
+	..
+	__
+	levels : std::size_t
+}
+smt_commandt <|-- smt_pop_commandt
+
+class smt_push_commandt {
+	""(push 1)""
+	..
+	__
+	levels : std::size_t
+}
+smt_commandt <|-- smt_push_commandt
+
+class smt_termt {
+	..
+	Section 3.6 page 26
+	Analogous to `exprt`.
+	Note - Protected constructor, so as to only allow construction as part of a
+	sub-class. Public copy/upcast/assignment to this class still available.
+	__
+	sort : smt_sortt
+}
+irept <|-- smt_termt
+smt_termt *-- smt_sortt
+
+class smt_optiont {
+	..
+	Note - Protected constructor, so as to only allow construction as part of a
+	sub-class. Public copy/upcast/assignment to this class still available.
+	__
+}
+irept <|-- smt_optiont
+
+class smt_option_produce_modelst {
+	:produce-models true
+	..
+	Section 4.1.7 page 56
+	__
+	value : bool
+}
+smt_optiont <|-- smt_option_produce_modelst
+
+class smt_logict {
+	..
+	Note - Protected constructor, so as to only allow construction as part of a
+	sub-class. Public copy/upcast/assignment to this class still available.
+	__
+}
+irept <|-- smt_logict
+
+class smt_logic_qf_aufbvt {
+	""QF_AUFBV""
+	..
+	https://smtlib.cs.uiowa.edu/logics-all.shtml
+	__
+}
+smt_logict <|-- smt_logic_qf_aufbvt
+
+class smt_bool_literal_termt {
+	""true""
+	""false""
+	..
+	Sort is set to smt_bool_sortt in constructor. Idea - factory member functions
+	for true and false.
+	__
+	value : bool
+}
+smt_termt <-- smt_bool_literal_termt
+
+class smt_bit_vector_constant_termt {
+	""(_ bv0 32)""
+	..
+	http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV - See bitvector constants
+	__
+	value : mp_integert
+	width : std::size_t
+}
+smt_termt <|-- smt_bit_vector_constant_termt
+
+class smt_identifier_termt {
+	""|main::1::x!0@1#1|""
+	..
+	__
+	value : irep_idt
+}
+smt_termt <|-- smt_identifier_termt
+
+class smt_not_termt {
+	(not false)
+	..
+	__
+	operand : smt_termt
+}
+smt_termt <|-- smt_not_termt
+smt_not_termt *-- smt_termt
+
+class smt_function_application_termt {
+	""(= x y)""
+	..
+	Section 3.6 page 27.
+	Sort checking should be carried out somewhere, to confirm that the sorts of
+	the term arguments match the sorts of the function definition.
+	__
+	function_identifier : irep_idt
+	arguments : std::vector<smt_termt>
+}
+smt_termt <|-- smt_function_application_termt
+
+class smt_sortt {
+	..
+	Section 3.5 page 26
+	Analogous to `typet`.
+	Note - Protected constructor, so as to only allow construction as part of a
+	sub-class. Public copy/upcast/assignment to this class still available.
+	__
+}
+irept <|-- smt_sortt
+
+class smt_bool_sortt {
+	""Bool""
+	..
+	Section 3.5 page 26
+	__
+}
+smt_sortt <|-- smt_bool_sortt
+
+class smt_bit_vector_sortt {
+	""(_ BitVec 32)""
+	..
+	http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml
+	__
+	bit_width : std::size_t
+}
+smt_sortt <|-- smt_bit_vector_sortt
+
+@enduml
diff --git a/src/solvers/smt2_incremental/smt_commands.cpp b/src/solvers/smt2_incremental/smt_commands.cpp
new file mode 100644
index 00000000000..45bfc418e38
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_commands.cpp
@@ -0,0 +1,197 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_commands.h>
+
+#include <util/range.h>
+
+// Define the irep_idts for commands.
+#define COMMAND_ID(the_id)                                                     \
+  const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
+#include <solvers/smt2_incremental/smt_commands.def>
+#undef COMMAND_ID
+
+bool smt_commandt::operator==(const smt_commandt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_commandt::operator!=(const smt_commandt &other) const
+{
+  return !(*this == other);
+}
+
+smt_assert_commandt::smt_assert_commandt(smt_termt condition)
+  : smt_commandt{ID_smt_assert_command}
+{
+  INVARIANT(
+    condition.get_sort() == smt_bool_sortt{},
+    "Only terms with boolean sorts can be asserted.");
+  set(ID_cond, upcast(std::move(condition)));
+}
+
+const smt_termt &smt_assert_commandt::condition() const
+{
+  return downcast(find(ID_cond));
+}
+
+smt_check_sat_commandt::smt_check_sat_commandt()
+  : smt_commandt{ID_smt_check_sat_command}
+{
+}
+
+smt_declare_function_commandt::smt_declare_function_commandt(
+  smt_identifier_termt identifier,
+  std::vector<smt_sortt> parameter_sorts)
+  : smt_commandt{ID_smt_declare_function_command}
+{
+  set(ID_identifier, term_storert::upcast(std::move(identifier)));
+  std::transform(
+    std::make_move_iterator(parameter_sorts.begin()),
+    std::make_move_iterator(parameter_sorts.end()),
+    std::back_inserter(get_sub()),
+    [](smt_sortt &&parameter_sort) {
+      return sort_storert::upcast(std::move(parameter_sort));
+    });
+}
+
+const smt_identifier_termt &smt_declare_function_commandt::identifier() const
+{
+  return static_cast<const smt_identifier_termt &>(
+    term_storert::downcast(find(ID_identifier)));
+}
+
+const smt_sortt &smt_declare_function_commandt::return_sort() const
+{
+  return identifier().get_sort();
+}
+
+std::vector<std::reference_wrapper<const smt_sortt>>
+smt_declare_function_commandt::parameter_sorts() const
+{
+  return make_range(get_sub()).map([](const irept &parameter_sort) {
+    return std::cref(sort_storert::downcast(parameter_sort));
+  });
+}
+
+smt_exit_commandt::smt_exit_commandt() : smt_commandt{ID_smt_exit_command}
+{
+}
+
+smt_define_function_commandt::smt_define_function_commandt(
+  irep_idt identifier,
+  std::vector<smt_identifier_termt> parameters,
+  smt_termt definition)
+  : smt_commandt{ID_smt_define_function_command}
+{
+  set(ID_identifier, identifier);
+  std::transform(
+    std::make_move_iterator(parameters.begin()),
+    std::make_move_iterator(parameters.end()),
+    std::back_inserter(get_sub()),
+    [](smt_identifier_termt &&parameter) {
+      return upcast(std::move(parameter));
+    });
+  set(ID_code, upcast(std::move(definition)));
+}
+
+const irep_idt &smt_define_function_commandt::identifier() const
+{
+  return get(ID_identifier);
+}
+
+std::vector<std::reference_wrapper<const smt_identifier_termt>>
+smt_define_function_commandt::parameters() const
+{
+  return make_range(get_sub()).map([](const irept &parameter) {
+    return std::cref(
+      static_cast<const smt_identifier_termt &>(downcast((parameter))));
+  });
+}
+
+const smt_sortt &smt_define_function_commandt::return_sort() const
+{
+  return definition().get_sort();
+}
+
+const smt_termt &smt_define_function_commandt::definition() const
+{
+  return downcast(find(ID_code));
+}
+
+smt_get_value_commandt::smt_get_value_commandt(smt_termt descriptor)
+  : smt_commandt{ID_smt_get_value_command}
+{
+  set(ID_value, upcast(std::move(descriptor)));
+}
+
+const smt_termt &smt_get_value_commandt::descriptor() const
+{
+  return downcast(find(ID_value));
+}
+
+smt_push_commandt::smt_push_commandt(std::size_t levels)
+  : smt_commandt(ID_smt_push_command)
+{
+  set_size_t(ID_value, levels);
+}
+
+size_t smt_push_commandt::levels() const
+{
+  return get_size_t(ID_value);
+}
+
+smt_pop_commandt::smt_pop_commandt(std::size_t levels)
+  : smt_commandt(ID_smt_pop_command)
+{
+  set_size_t(ID_value, levels);
+}
+
+size_t smt_pop_commandt::levels() const
+{
+  return get_size_t(ID_value);
+}
+
+smt_set_logic_commandt::smt_set_logic_commandt(smt_logict logic)
+  : smt_commandt(ID_smt_set_logic_command)
+{
+  set(ID_value, upcast(std::move(logic)));
+}
+
+const smt_logict &smt_set_logic_commandt::logic() const
+{
+  return downcast(find(ID_value));
+}
+
+smt_set_option_commandt::smt_set_option_commandt(smt_optiont option)
+  : smt_commandt(ID_smt_set_option_command)
+{
+  set(ID_value, upcast(std::move(option)));
+}
+
+const smt_optiont &smt_set_option_commandt::option() const
+{
+  return downcast(find(ID_value));
+}
+
+template <typename visitort>
+void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
+{
+#define COMMAND_ID(the_id)                                                     \
+  if(id == ID_smt_##the_id##_command)                                          \
+    return visitor.visit(static_cast<const smt_##the_id##_commandt &>(command));
+// The include below is marked as nolint because including the same file
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_commands.def> // NOLINT(build/include)
+#undef COMMAND_ID
+  UNREACHABLE;
+}
+
+void smt_commandt::accept(smt_command_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_commandt::accept(smt_command_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}
diff --git a/src/solvers/smt2_incremental/smt_commands.def b/src/solvers/smt2_incremental/smt_commands.def
new file mode 100644
index 00000000000..4d664b629cc
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_commands.def
@@ -0,0 +1,18 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of commands which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the command classes.
+///  * The member functions of the `smt_command_const_downcast_visitort` class.
+///  * The type of command checks required to implement `smt_commandt::accept`.
+COMMAND_ID(assert)
+COMMAND_ID(check_sat)
+COMMAND_ID(declare_function)
+COMMAND_ID(define_function)
+COMMAND_ID(exit)
+COMMAND_ID(get_value)
+COMMAND_ID(pop)
+COMMAND_ID(push)
+COMMAND_ID(set_logic)
+COMMAND_ID(set_option)
diff --git a/src/solvers/smt2_incremental/smt_commands.h b/src/solvers/smt2_incremental/smt_commands.h
new file mode 100644
index 00000000000..2b06f5b9fa5
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_commands.h
@@ -0,0 +1,135 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
+
+#include <solvers/smt2_incremental/smt_logics.h>
+#include <solvers/smt2_incremental/smt_options.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <util/irep.h>
+
+class smt_command_const_downcast_visitort;
+
+class smt_commandt : protected irept
+{
+public:
+  // smt_commandt does not support the notion of an empty / null state. Use
+  // optionalt<smt_commandt> instead if an empty command is required.
+  smt_commandt() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_commandt &) const;
+  bool operator!=(const smt_commandt &) const;
+
+  void accept(smt_command_const_downcast_visitort &) const;
+  void accept(smt_command_const_downcast_visitort &&) const;
+
+protected:
+  using irept::irept;
+};
+
+class smt_assert_commandt : public smt_commandt,
+                            private smt_termt::storert<smt_assert_commandt>
+{
+public:
+  explicit smt_assert_commandt(smt_termt condition);
+  const smt_termt &condition() const;
+};
+
+class smt_check_sat_commandt : public smt_commandt
+{
+public:
+  smt_check_sat_commandt();
+};
+
+class smt_declare_function_commandt
+  : public smt_commandt,
+    private smt_sortt::storert<smt_declare_function_commandt>,
+    private smt_termt::storert<smt_declare_function_commandt>
+{
+public:
+  smt_declare_function_commandt(
+    smt_identifier_termt identifier,
+    std::vector<smt_sortt> parameter_sorts);
+  const smt_identifier_termt &identifier() const;
+  const smt_sortt &return_sort() const;
+  std::vector<std::reference_wrapper<const smt_sortt>> parameter_sorts() const;
+
+private:
+  using sort_storert = smt_sortt::storert<smt_declare_function_commandt>;
+  using term_storert = smt_termt::storert<smt_declare_function_commandt>;
+};
+
+class smt_define_function_commandt
+  : public smt_commandt,
+    private smt_termt::storert<smt_define_function_commandt>
+{
+public:
+  smt_define_function_commandt(
+    irep_idt identifier,
+    std::vector<smt_identifier_termt> parameters,
+    smt_termt definition);
+  const irep_idt &identifier() const;
+  std::vector<std::reference_wrapper<const smt_identifier_termt>>
+  parameters() const;
+  const smt_sortt &return_sort() const;
+  const smt_termt &definition() const;
+};
+
+class smt_exit_commandt : public smt_commandt
+{
+public:
+  smt_exit_commandt();
+};
+
+class smt_get_value_commandt : public smt_commandt,
+                               protected smt_termt::storert<smt_assert_commandt>
+{
+public:
+  explicit smt_get_value_commandt(smt_termt descriptor);
+  const smt_termt &descriptor() const;
+};
+
+class smt_push_commandt : public smt_commandt
+{
+public:
+  explicit smt_push_commandt(std::size_t levels);
+  size_t levels() const;
+};
+
+class smt_pop_commandt : public smt_commandt
+{
+public:
+  explicit smt_pop_commandt(std::size_t levels);
+  size_t levels() const;
+};
+
+class smt_set_logic_commandt
+  : public smt_commandt,
+    private smt_logict::storert<smt_set_logic_commandt>
+{
+public:
+  explicit smt_set_logic_commandt(smt_logict logic);
+  const smt_logict &logic() const;
+};
+
+class smt_set_option_commandt
+  : public smt_commandt,
+    private smt_optiont::storert<smt_set_option_commandt>
+{
+public:
+  explicit smt_set_option_commandt(smt_optiont option);
+  const smt_optiont &option() const;
+};
+
+class smt_command_const_downcast_visitort
+{
+public:
+#define COMMAND_ID(the_id)                                                     \
+  virtual void visit(const smt_##the_id##_commandt &) = 0;
+#include "smt_commands.def"
+#undef COMMAND_ID
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H
diff --git a/src/solvers/smt2_incremental/smt_logics.cpp b/src/solvers/smt2_incremental/smt_logics.cpp
new file mode 100644
index 00000000000..22656038e68
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_logics.cpp
@@ -0,0 +1,47 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_logics.h>
+
+// Define the irep_idts for logics.
+#define LOGIC_ID(the_id)                                                       \
+  const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
+#include <solvers/smt2_incremental/smt_logics.def>
+#undef LOGIC_ID
+
+bool smt_logict::operator==(const smt_logict &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_logict::operator!=(const smt_logict &other) const
+{
+  return !(*this == other);
+}
+
+template <typename visitort>
+void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
+{
+#define LOGIC_ID(the_id)                                                       \
+  if(id == ID_smt_logic_##the_id)                                              \
+    return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
+// The include below is marked as nolint because including the same file
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_logics.def> // NOLINT(build/include)
+#undef LOGIC_ID
+  UNREACHABLE;
+}
+
+void smt_logict::accept(smt_logic_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_logict::accept(smt_logic_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}
+
+smt_logic_quantifier_free_bit_vectorst::smt_logic_quantifier_free_bit_vectorst()
+  : smt_logict{ID_smt_logic_quantifier_free_bit_vectors}
+{
+}
diff --git a/src/solvers/smt2_incremental/smt_logics.def b/src/solvers/smt2_incremental/smt_logics.def
new file mode 100644
index 00000000000..15593bdb68b
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_logics.def
@@ -0,0 +1,9 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of options which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the logic classes.
+///  * The member functions of the `smt_logic_const_downcast_visitort` class.
+///  * The type of option checks required to implement `smt_logict::accept`.
+LOGIC_ID(quantifier_free_bit_vectors)
diff --git a/src/solvers/smt2_incremental/smt_logics.h b/src/solvers/smt2_incremental/smt_logics.h
new file mode 100644
index 00000000000..97f47473315
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_logics.h
@@ -0,0 +1,78 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_LOGICS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_LOGICS_H
+
+class smt_logic_const_downcast_visitort;
+
+#include <util/irep.h>
+
+class smt_logict : protected irept
+{
+public:
+  // smt_logict does not support the notion of an empty / null state. Use
+  // optionalt<smt_logict> instead if an empty logic is required.
+  smt_logict() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_logict &) const;
+  bool operator!=(const smt_logict &) const;
+
+  void accept(smt_logic_const_downcast_visitort &) const;
+  void accept(smt_logic_const_downcast_visitort &&) const;
+
+  /// \brief Class for adding the ability to up and down cast smt_logict to and
+  ///   from irept. These casts are required by other irept derived classes in
+  ///   order to store instances of smt_logict inside them.
+  /// \tparam derivedt The type of class which derives from this class and from
+  ///   irept.
+  template <typename derivedt>
+  class storert
+  {
+  protected:
+    storert();
+    static irept upcast(smt_logict logic);
+    static const smt_logict &downcast(const irept &);
+  };
+
+protected:
+  using irept::irept;
+};
+
+template <typename derivedt>
+smt_logict::storert<derivedt>::storert()
+{
+  static_assert(
+    std::is_base_of<irept, derivedt>::value &&
+      std::is_base_of<storert<derivedt>, derivedt>::value,
+    "Only irept based classes need to upcast smt_termt to store it.");
+}
+
+template <typename derivedt>
+irept smt_logict::storert<derivedt>::upcast(smt_logict logic)
+{
+  return static_cast<irept &&>(std::move(logic));
+}
+
+template <typename derivedt>
+const smt_logict &smt_logict::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_logict &>(irep);
+}
+
+class smt_logic_quantifier_free_bit_vectorst : public smt_logict
+{
+public:
+  smt_logic_quantifier_free_bit_vectorst();
+};
+
+class smt_logic_const_downcast_visitort
+{
+public:
+#define LOGIC_ID(the_id) virtual void visit(const smt_logic_##the_id##t &) = 0;
+#include "smt_logics.def"
+#undef LOGIC_ID
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_LOGICS_H
diff --git a/src/solvers/smt2_incremental/smt_options.cpp b/src/solvers/smt2_incremental/smt_options.cpp
new file mode 100644
index 00000000000..f047003472d
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_options.cpp
@@ -0,0 +1,57 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_options.h>
+
+// Define the irep_idts for options.
+#define OPTION_ID(the_id)                                                      \
+  const irep_idt ID_smt_option_##the_id{"smt_option_" #the_id};
+#include <solvers/smt2_incremental/smt_options.def>
+#undef OPTION_ID
+
+smt_optiont::smt_optiont(const irep_idt id) : irept(id)
+{
+}
+
+bool smt_optiont::operator==(const smt_optiont &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_optiont::operator!=(const smt_optiont &other) const
+{
+  return !(*this == other);
+}
+
+smt_option_produce_modelst::smt_option_produce_modelst(bool setting)
+  : smt_optiont{ID_smt_option_produce_models}
+{
+  set(ID_value, setting);
+}
+
+bool smt_option_produce_modelst::setting() const
+{
+  return get_bool(ID_value);
+}
+
+template <typename visitort>
+void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
+{
+#define OPTION_ID(the_id)                                                      \
+  if(id == ID_smt_option_##the_id)                                             \
+    return visitor.visit(static_cast<const smt_option_##the_id##t &>(option));
+// The include below is marked as nolint because including the same file
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_options.def> // NOLINT(build/include)
+#undef OPTION_ID
+  UNREACHABLE;
+}
+
+void smt_optiont::accept(smt_option_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_optiont::accept(smt_option_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}
diff --git a/src/solvers/smt2_incremental/smt_options.def b/src/solvers/smt2_incremental/smt_options.def
new file mode 100644
index 00000000000..3462b98b2f6
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_options.def
@@ -0,0 +1,9 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of options which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the option classes.
+///  * The member functions of the `smt_option_const_downcast_visitort` class.
+///  * The type of option checks required to implement `smt_optiont::accept`.
+OPTION_ID(produce_models)
diff --git a/src/solvers/smt2_incremental/smt_options.h b/src/solvers/smt2_incremental/smt_options.h
new file mode 100644
index 00000000000..b65f0384d66
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_options.h
@@ -0,0 +1,80 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
+
+#include <util/irep.h>
+
+class smt_option_const_downcast_visitort;
+
+class smt_optiont : protected irept
+{
+public:
+  // smt_optiont does not support the notion of an empty / null state. Use
+  // optionalt<smt_optiont> instead if an empty option is required.
+  smt_optiont() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_optiont &) const;
+  bool operator!=(const smt_optiont &) const;
+
+  void accept(smt_option_const_downcast_visitort &) const;
+  void accept(smt_option_const_downcast_visitort &&) const;
+
+  /// \brief Class for adding the ability to up and down cast smt_optiont to and
+  ///   from irept. These casts are required by other irept derived classes in
+  ///   order to store instances of smt_optiont inside them.
+  /// \tparam derivedt The type of class which derives from this class and from
+  ///   irept.
+  template <typename derivedt>
+  class storert
+  {
+  protected:
+    storert();
+    static irept upcast(smt_optiont option);
+    static const smt_optiont &downcast(const irept &);
+  };
+
+protected:
+  explicit smt_optiont(irep_idt id);
+};
+
+template <typename derivedt>
+smt_optiont::storert<derivedt>::storert()
+{
+  static_assert(
+    std::is_base_of<irept, derivedt>::value &&
+      std::is_base_of<storert<derivedt>, derivedt>::value,
+    "Only irept based classes need to upcast smt_termt to store it.");
+}
+
+template <typename derivedt>
+irept smt_optiont::storert<derivedt>::upcast(smt_optiont option)
+{
+  return static_cast<irept &&>(std::move(option));
+}
+
+template <typename derivedt>
+const smt_optiont &smt_optiont::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_optiont &>(irep);
+}
+
+class smt_option_produce_modelst : public smt_optiont
+{
+public:
+  explicit smt_option_produce_modelst(bool setting);
+  bool setting() const;
+};
+
+class smt_option_const_downcast_visitort
+{
+public:
+#define OPTION_ID(the_id)                                                      \
+  virtual void visit(const smt_option_##the_id##t &) = 0;
+#include "smt_options.def"
+#undef OPTION_ID
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
diff --git a/src/solvers/smt2_incremental/smt_sorts.cpp b/src/solvers/smt2_incremental/smt_sorts.cpp
new file mode 100644
index 00000000000..bc721afd061
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_sorts.cpp
@@ -0,0 +1,57 @@
+// Author: Diffblue Ltd.
+
+#include "smt_sorts.h"
+
+#include <util/invariant.h>
+
+// Define the irep_idts for sorts.
+#define SORT_ID(the_id)                                                        \
+  const irep_idt ID_smt_##the_id##_sort{"smt_" #the_id "_sort"};
+#include <solvers/smt2_incremental/smt_sorts.def>
+#undef SORT_ID
+
+bool smt_sortt::operator==(const smt_sortt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_sortt::operator!=(const smt_sortt &other) const
+{
+  return !(*this == other);
+}
+
+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}
+{
+  set_size_t(ID_width, bit_width);
+}
+
+std::size_t smt_bit_vector_sortt::bit_width() const
+{
+  return get_size_t(ID_width);
+}
+
+template <typename visitort>
+void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
+{
+#define SORT_ID(the_id)                                                        \
+  if(id == ID_smt_##the_id##_sort)                                             \
+    return visitor.visit(static_cast<const smt_##the_id##_sortt &>(sort));
+#include "smt_sorts.def"
+#undef SORT_ID
+  UNREACHABLE;
+}
+
+void smt_sortt::accept(smt_sort_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_sortt::accept(smt_sort_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}
diff --git a/src/solvers/smt2_incremental/smt_sorts.def b/src/solvers/smt2_incremental/smt_sorts.def
new file mode 100644
index 00000000000..1bb57e4379b
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_sorts.def
@@ -0,0 +1,10 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of sorts which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the sort classes.
+///  * The member functions of the `smt_sort_const_downcast_visitort` class.
+///  * The type of sort checks required to implement `smt_sortt::accept`.
+SORT_ID(bool)
+SORT_ID(bit_vector)
diff --git a/src/solvers/smt2_incremental/smt_sorts.h b/src/solvers/smt2_incremental/smt_sorts.h
new file mode 100644
index 00000000000..ae5244b984f
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_sorts.h
@@ -0,0 +1,91 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Data structure for smt sorts.
+/// \note All classes derived from `smt_sortt`, must be listed in smt_sorts.def.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
+
+#include <util/irep.h>
+
+#include <type_traits>
+
+class smt_sort_const_downcast_visitort;
+
+class smt_sortt : protected irept
+{
+public:
+  // smt_sortt does not support the notion of an empty / null state. Use
+  // optionalt<smt_sortt> instead if an empty sort is required.
+  smt_sortt() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_sortt &) const;
+  bool operator!=(const smt_sortt &) const;
+
+  void accept(smt_sort_const_downcast_visitort &) const;
+  void accept(smt_sort_const_downcast_visitort &&) const;
+
+  /// \brief Class for adding the ability to up and down cast smt_sortt to and
+  ///   from irept. These casts are required by other irept derived classes in
+  ///   order to store instances of smt_sortt inside them.
+  /// \tparam derivedt The type of class which derives from this class and from
+  ///   irept.
+  template <typename derivedt>
+  class storert
+  {
+  protected:
+    storert();
+    static irept upcast(smt_sortt sort);
+    static const smt_sortt &downcast(const irept &);
+  };
+
+protected:
+  using irept::irept;
+};
+
+template <typename derivedt>
+smt_sortt::storert<derivedt>::storert()
+{
+  static_assert(
+    std::is_base_of<irept, derivedt>::value &&
+      std::is_base_of<storert<derivedt>, derivedt>::value,
+    "Only irept based classes need to upcast smt_sortt to store it.");
+}
+
+template <typename derivedt>
+irept smt_sortt::storert<derivedt>::upcast(smt_sortt sort)
+{
+  return static_cast<irept &&>(std::move(sort));
+}
+
+template <typename derivedt>
+const smt_sortt &smt_sortt::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_sortt &>(irep);
+}
+
+class smt_bool_sortt final : public smt_sortt
+{
+public:
+  smt_bool_sortt();
+};
+
+class smt_bit_vector_sortt final : public smt_sortt
+{
+public:
+  explicit smt_bit_vector_sortt(std::size_t bit_width);
+  std::size_t bit_width() const;
+};
+
+class smt_sort_const_downcast_visitort
+{
+public:
+#define SORT_ID(the_id) virtual void visit(const smt_##the_id##_sortt &) = 0;
+#include "smt_sorts.def"
+#undef SORT_ID
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp
new file mode 100644
index 00000000000..8c631ff6ffb
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_terms.cpp
@@ -0,0 +1,166 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+
+#include <util/arith_tools.h>
+#include <util/mp_arith.h>
+#include <util/range.h>
+
+#include <algorithm>
+#include <regex>
+
+// Define the irep_idts for terms.
+#define TERM_ID(the_id)                                                        \
+  const irep_idt ID_smt_##the_id##_term{"smt_" #the_id "_term"};
+#include <solvers/smt2_incremental/smt_terms.def>
+#undef TERM_ID
+
+smt_termt::smt_termt(irep_idt id, smt_sortt sort)
+  : irept{id, {{ID_type, upcast(std::move(sort))}}, {}}
+{
+}
+
+bool smt_termt::operator==(const smt_termt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_termt::operator!=(const smt_termt &other) const
+{
+  return !(*this == other);
+}
+
+const smt_sortt &smt_termt::get_sort() const
+{
+  return downcast(find(ID_type));
+}
+
+smt_bool_literal_termt::smt_bool_literal_termt(bool value)
+  : smt_termt{ID_smt_bool_literal_term, smt_bool_sortt{}}
+{
+  set(ID_value, value);
+}
+
+bool smt_bool_literal_termt::value() const
+{
+  return get_bool(ID_value);
+}
+
+smt_not_termt::smt_not_termt(smt_termt operand)
+  : smt_termt{ID_smt_not_term, smt_bool_sortt{}}
+{
+  INVARIANT(
+    operand.get_sort() == smt_bool_sortt{},
+    "smt_not_termt may only be applied to terms which have bool sort.");
+  get_sub().push_back(std::move(operand));
+}
+
+const smt_termt &smt_not_termt::operand() const
+{
+  return static_cast<const smt_termt &>(get_sub().at(0));
+}
+
+static bool is_valid_smt_identifier(irep_idt identifier)
+{
+  static const std::regex valid{R"(^[^\|\\]*$)"};
+  return std::regex_match(id2string(identifier), valid);
+}
+
+smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
+  : smt_termt(ID_smt_identifier_term, std::move(sort))
+{
+  INVARIANT(
+    is_valid_smt_identifier(identifier),
+    R"(Identifiers may not contain | or \ characters.)");
+  set(ID_identifier, identifier);
+}
+
+irep_idt smt_identifier_termt::identifier() const
+{
+  return get(ID_identifier);
+}
+
+smt_bit_vector_constant_termt::smt_bit_vector_constant_termt(
+  const mp_integer &value,
+  smt_bit_vector_sortt sort)
+  : smt_termt{ID_smt_bit_vector_constant_term, std::move(sort)}
+{
+  INVARIANT(
+    value < power(mp_integer{2}, get_sort().bit_width()),
+    "value must fit in number of bits available.");
+  INVARIANT(
+    !value.is_negative(),
+    "Negative numbers are not supported by bit vector constants.");
+  set(ID_value, integer2bvrep(value, get_sort().bit_width()));
+}
+
+smt_bit_vector_constant_termt::smt_bit_vector_constant_termt(
+  const mp_integer &value,
+  std::size_t bit_width)
+  : smt_bit_vector_constant_termt{value, smt_bit_vector_sortt{bit_width}}
+{
+}
+
+mp_integer smt_bit_vector_constant_termt::value() const
+{
+  return bvrep2integer(get(ID_value), get_sort().bit_width(), false);
+}
+
+const smt_bit_vector_sortt &smt_bit_vector_constant_termt::get_sort() const
+{
+  // The below cast is sound because the constructor only allows bit_vector
+  // sorts to be set.
+  return static_cast<const smt_bit_vector_sortt &>(smt_termt::get_sort());
+}
+
+smt_function_application_termt::smt_function_application_termt(
+  smt_identifier_termt function_identifier,
+  std::vector<smt_termt> arguments)
+  : smt_termt(ID_smt_function_application_term, function_identifier.get_sort())
+{
+  set(ID_identifier, std::move(function_identifier));
+  std::transform(
+    std::make_move_iterator(arguments.begin()),
+    std::make_move_iterator(arguments.end()),
+    std::back_inserter(get_sub()),
+    [](smt_termt &&argument) { return static_cast<irept &&>(argument); });
+}
+
+const smt_identifier_termt &
+smt_function_application_termt::function_identifier() const
+{
+  return static_cast<const smt_identifier_termt &>(find(ID_identifier));
+}
+
+std::vector<std::reference_wrapper<const smt_termt>>
+smt_function_application_termt::arguments() const
+{
+  return make_range(get_sub()).map([](const irept &argument) {
+    return std::cref(static_cast<const smt_termt &>(argument));
+  });
+}
+
+template <typename visitort>
+void accept(const smt_termt &term, const irep_idt &id, visitort &&visitor)
+{
+#define TERM_ID(the_id)                                                        \
+  if(id == ID_smt_##the_id##_term)                                             \
+    return visitor.visit(static_cast<const smt_##the_id##_termt &>(term));
+// The include below is marked as nolint because including the same file
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_terms.def> // NOLINT(build/include)
+#undef TERM_ID
+  UNREACHABLE;
+}
+
+void smt_termt::accept(smt_term_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_termt::accept(smt_term_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}
diff --git a/src/solvers/smt2_incremental/smt_terms.def b/src/solvers/smt2_incremental/smt_terms.def
new file mode 100644
index 00000000000..77b5f210225
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_terms.def
@@ -0,0 +1,13 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of terms which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the term classes.
+///  * The member functions of the `smt_term_const_downcast_visitort` class.
+///  * The type of term checks required to implement `smt_termt::accept`.
+TERM_ID(bool_literal)
+TERM_ID(not)
+TERM_ID(identifier)
+TERM_ID(bit_vector_constant)
+TERM_ID(function_application)
diff --git a/src/solvers/smt2_incremental/smt_terms.h b/src/solvers/smt2_incremental/smt_terms.h
new file mode 100644
index 00000000000..f6b4d611a1e
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_terms.h
@@ -0,0 +1,139 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+#include <util/irep.h>
+
+#include <functional>
+
+class BigInt;
+using mp_integer = BigInt;
+
+class smt_term_const_downcast_visitort;
+class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
+{
+public:
+  // smt_termt does not support the notion of an empty / null state. Use
+  // optionalt<smt_termt> instead if an empty term is required.
+  smt_termt() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_termt &) const;
+  bool operator!=(const smt_termt &) const;
+
+  const smt_sortt &get_sort() const;
+
+  void accept(smt_term_const_downcast_visitort &) const;
+  void accept(smt_term_const_downcast_visitort &&) const;
+
+  /// \brief Class for adding the ability to up and down cast smt_termt to and
+  ///   from irept. These casts are required by other irept derived classes in
+  ///   order to store instances of smt_termt inside them.
+  /// \tparam derivedt The type of class which derives from this class and from
+  ///   irept.
+  template <typename derivedt>
+  class storert
+  {
+  protected:
+    storert();
+    static irept upcast(smt_termt term);
+    static const smt_termt &downcast(const irept &);
+  };
+
+protected:
+  smt_termt(irep_idt id, smt_sortt sort);
+};
+
+template <typename derivedt>
+smt_termt::storert<derivedt>::storert()
+{
+  static_assert(
+    std::is_base_of<irept, derivedt>::value &&
+      std::is_base_of<storert<derivedt>, derivedt>::value,
+    "Only irept based classes need to upcast smt_termt to store it.");
+}
+
+template <typename derivedt>
+irept smt_termt::storert<derivedt>::upcast(smt_termt term)
+{
+  return static_cast<irept &&>(std::move(term));
+}
+
+template <typename derivedt>
+const smt_termt &smt_termt::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_termt &>(irep);
+}
+
+class smt_bool_literal_termt : public smt_termt
+{
+public:
+  explicit smt_bool_literal_termt(bool value);
+  bool value() const;
+};
+
+class smt_not_termt : public smt_termt
+{
+public:
+  explicit smt_not_termt(smt_termt operand);
+  const smt_termt &operand() const;
+};
+
+/// Stores identifiers in unescaped and unquoted form. Any escaping or quoting
+/// required should be performed during printing.
+class smt_identifier_termt : public smt_termt
+{
+public:
+  /// \brief Constructs an identifier term with the given \p identifier and
+  ///   \p sort.
+  /// \param identifier: This should be the unescaped form of the identifier.
+  ///   Escaping of the identifier if required is to be performed as part of the
+  ///   printing operation. The given identifier is checked to ensure that it
+  ///   has not already been escaped, in order to avoid escaping it twice.
+  ///   Performing escaping during the printing will ensure that the identifiers
+  ///   output conform to the specification of the concrete form.
+  /// \param sort: The sort which this term will have. All terms in our abstract
+  ///   form must be sorted, even if those sorts are not printed in all
+  ///   contexts.
+  smt_identifier_termt(irep_idt identifier, smt_sortt sort);
+  irep_idt identifier() const;
+};
+
+class smt_bit_vector_constant_termt : public smt_termt
+{
+public:
+  smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt);
+  smt_bit_vector_constant_termt(const mp_integer &value, std::size_t bit_width);
+  mp_integer value() const;
+
+  // This deliberately hides smt_termt::get_sort, because bit_vector terms
+  // always have bit_vector sorts. The same sort data is returned for both
+  // functions either way. Therefore this hiding is benign if the kind of sort
+  // is not important and useful for avoiding casts if the term is a known
+  // smt_bit_vector_constant_termt at compile time and the `bit_width()` is
+  // needed.
+  const smt_bit_vector_sortt &get_sort() const;
+};
+
+class smt_function_application_termt : public smt_termt
+{
+public:
+  smt_function_application_termt(
+    smt_identifier_termt function_identifier,
+    std::vector<smt_termt> arguments);
+  const smt_identifier_termt &function_identifier() const;
+  std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
+};
+
+class smt_term_const_downcast_visitort
+{
+public:
+#define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
+#include "smt_terms.def"
+#undef TERM_ID
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
diff --git a/unit/Makefile b/unit/Makefile
index 324cfcd00ad..46fab54b042 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -85,6 +85,9 @@ SRC += analyses/ai/ai.cpp \
        solvers/sat/satcheck_cadical.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/smt2/smt2_conv.cpp \
+       solvers/smt2_incremental/smt_commands.cpp \
+       solvers/smt2_incremental/smt_sorts.cpp \
+       solvers/smt2_incremental/smt_terms.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 \
@@ -249,10 +252,7 @@ ifeq ($(CADICAL),)
 EXCLUDED_TESTS += satcheck_cadical.cpp
 endif
 
-N_CATCH_TESTS = $(shell \
-                  cat $$(find . -name "*.cpp" \
-                $$(printf ' -not -name %s ' $(EXCLUDED_TESTS))) | \
-                  grep -E "(SCENARIO|TEST_CASE)" | grep -c -v '\[\.\]')
+N_CATCH_TESTS = $(shell ./count_tests.py --exclude-files "$(EXCLUDED_TESTS)")
 
 memory-analyzer/input.inc: memory-analyzer/input.txt
 	../src/ansi-c/file_converter$(EXEEXT) $< > $@
diff --git a/unit/count_tests.py b/unit/count_tests.py
new file mode 100755
index 00000000000..314f4984113
--- /dev/null
+++ b/unit/count_tests.py
@@ -0,0 +1,68 @@
+#!/usr/bin/env python3
+#
+# Count number of unit tests.
+#
+
+import argparse
+import os
+import sys
+
+
+class argument_separator_countert:
+    def __init__(self):
+        self.bracket_depth = 0
+        self.separators = 0
+
+    def read_text(self, text):
+        for character in text:
+            if character == '(' or character == '<':
+                self.bracket_depth += 1
+            elif character == ')' or character == '(':
+                self.bracket_depth -= 1
+            elif character == ',' and self.bracket_depth == 1:
+                self.separators += 1
+
+
+def tests_in_file(file_path):
+    file_test_count = 0
+    template_counter = None
+    with open(file_path, "rt") as file:
+        for line in file:
+            if template_counter is None:
+                if line.startswith("TEST_CASE"):
+                    file_test_count += 1
+                if line.startswith("SCENARIO"):
+                    file_test_count += 1
+                if line.startswith("TEMPLATE_TEST_CASE"):
+                    template_counter = argument_separator_countert()
+                    template_counter.read_text(line)
+            else:
+                template_counter.read_text(line)
+            if template_counter is not None and template_counter.bracket_depth == 0:
+                file_test_count += (template_counter.separators - 1)
+                template_counter = None
+    return file_test_count
+
+
+def count_tests_in_directory(directory_path, exclude_files):
+    test_count = 0
+    for root, sub_directories, files in os.walk("."):
+        for file_name in files:
+            if any(file_name == excluded_file for excluded_file in exclude_files):
+                continue
+            _, extension = os.path.splitext(file_name)
+            if extension == ".cpp":
+                test_count += tests_in_file(os.path.join(root, file_name))
+    return test_count
+
+
+def main():
+    argument_parser = argparse.ArgumentParser()
+    argument_parser.add_argument("--exclude-files", dest="exclude_files", nargs=1, default=[""])
+    arguments = argument_parser.parse_args()
+    excluded_files = arguments.exclude_files[0].split()
+    print(count_tests_in_directory(".", exclude_files=excluded_files))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/unit/solvers/smt2_incremental/module_dependencies.txt b/unit/solvers/smt2_incremental/module_dependencies.txt
new file mode 100644
index 00000000000..9eb596f2a5c
--- /dev/null
+++ b/unit/solvers/smt2_incremental/module_dependencies.txt
@@ -0,0 +1,3 @@
+solvers/smt2_incremental
+testing-utils
+util
diff --git a/unit/solvers/smt2_incremental/smt_commands.cpp b/unit/solvers/smt2_incremental/smt_commands.cpp
new file mode 100644
index 00000000000..8aefb52a1f9
--- /dev/null
+++ b/unit/solvers/smt2_incremental/smt_commands.cpp
@@ -0,0 +1,94 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_commands.h>
+
+TEST_CASE("Test smt_commandt.pretty is accessible.", "[core][smt2_incremental]")
+{
+  const smt_commandt check_sat_command{smt_check_sat_commandt{}};
+  REQUIRE(check_sat_command.pretty(0, 0) == "smt_check_sat_command");
+}
+
+TEST_CASE("smt_assert_commandt condition getter", "[core][smt2_incremental]")
+{
+  const smt_assert_commandt assert_command{smt_bool_literal_termt{true}};
+  REQUIRE(assert_command.condition() == smt_bool_literal_termt{true});
+}
+
+TEST_CASE("smt_declare_function_commandt getters", "[core][smt2_incremental]")
+{
+  const smt_identifier_termt plus{"+", smt_bit_vector_sortt{9}};
+  const smt_declare_function_commandt function_declaration{
+    plus,
+    std::vector<smt_sortt>{smt_bit_vector_sortt{8}, smt_bit_vector_sortt{7}}};
+  CHECK(function_declaration.identifier() == plus);
+  CHECK(function_declaration.return_sort() == smt_bit_vector_sortt{9});
+  CHECK(
+    function_declaration.parameter_sorts()[0].get() == smt_bit_vector_sortt{8});
+  CHECK(
+    function_declaration.parameter_sorts()[1].get() == smt_bit_vector_sortt{7});
+}
+
+TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]")
+{
+  const smt_define_function_commandt function_definition{
+    "not first",
+    {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.parameters()[0].get() ==
+    smt_identifier_termt{"x", smt_bool_sortt{}});
+  CHECK(
+    function_definition.parameters()[1].get() ==
+    smt_identifier_termt{"y", smt_bool_sortt{}});
+  CHECK(
+    function_definition.definition() ==
+    smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}});
+}
+
+TEST_CASE("smt_get_value_commandt getter", "[core][smt2_incremental]")
+{
+  const smt_get_value_commandt get_value_command{
+    smt_identifier_termt{"x", smt_bool_sortt{}}};
+  REQUIRE(
+    get_value_command.descriptor() ==
+    smt_identifier_termt{"x", smt_bool_sortt{}});
+}
+
+TEST_CASE("smt_commandt equality", "[core][smt2_incremental]")
+{
+  const smt_exit_commandt exit_command{};
+  CHECK(exit_command == smt_exit_commandt{});
+  const smt_check_sat_commandt check_sat_command{};
+  CHECK(check_sat_command == smt_check_sat_commandt{});
+  CHECK_FALSE(exit_command == check_sat_command);
+  const smt_assert_commandt assert_true{smt_bool_literal_termt{true}};
+  CHECK(assert_true == smt_assert_commandt{smt_bool_literal_termt{true}});
+  const smt_assert_commandt assert_false{smt_bool_literal_termt{false}};
+  CHECK_FALSE(assert_true == assert_false);
+}
+
+TEST_CASE("smt_push_commandt level", "[core][smt2_incremental]")
+{
+  CHECK(smt_push_commandt(1).levels() == 1);
+  CHECK(smt_push_commandt(2).levels() == 2);
+}
+
+TEST_CASE("smt_pop_commandt level", "[core][smt2_incremental]")
+{
+  CHECK(smt_pop_commandt(1).levels() == 1);
+  CHECK(smt_pop_commandt(2).levels() == 2);
+}
+
+TEST_CASE("smt_set_option_commandt getter", "[core][smt2_incremental]")
+{
+  const auto models_on = smt_option_produce_modelst{true};
+  const auto models_off = smt_option_produce_modelst{false};
+  CHECK(models_on.setting() == true);
+  CHECK(models_off.setting() == false);
+  CHECK(smt_set_option_commandt{models_on}.option() == models_on);
+  CHECK(smt_set_option_commandt{models_off}.option() == models_off);
+}
diff --git a/unit/solvers/smt2_incremental/smt_sorts.cpp b/unit/solvers/smt2_incremental/smt_sorts.cpp
new file mode 100644
index 00000000000..94f532d3ece
--- /dev/null
+++ b/unit/solvers/smt2_incremental/smt_sorts.cpp
@@ -0,0 +1,78 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+
+TEST_CASE("Test smt_sortt.pretty is accessible.", "[core][smt2_incremental]")
+{
+  const smt_sortt bool_sort = smt_bool_sortt{};
+  REQUIRE(bool_sort.pretty(0, 0) == "smt_bool_sort");
+}
+
+TEST_CASE(
+  "Test smt_bit_vec_sortt bit_width getter.",
+  "[core][smt2_incremental]")
+{
+  REQUIRE(smt_bit_vector_sortt{32}.bit_width() == 32);
+}
+
+TEST_CASE("Visiting smt_bool_sortt.", "[core][smt2_incremental]")
+{
+  class : public smt_sort_const_downcast_visitort
+  {
+  public:
+    bool bool_visited = false;
+    bool bit_vec_visited = false;
+
+    void visit(const smt_bool_sortt &) override
+    {
+      bool_visited = true;
+    }
+
+    void visit(const smt_bit_vector_sortt &) override
+    {
+      bit_vec_visited = true;
+    }
+  } visitor;
+  smt_bool_sortt{}.accept(visitor);
+  REQUIRE(visitor.bool_visited);
+  REQUIRE_FALSE(visitor.bit_vec_visited);
+}
+
+TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
+{
+  class : public smt_sort_const_downcast_visitort
+  {
+  public:
+    bool bool_visited = false;
+    bool bit_vec_visited = false;
+
+    void visit(const smt_bool_sortt &) override
+    {
+      bool_visited = true;
+    }
+
+    void visit(const smt_bit_vector_sortt &bit_vec) override
+    {
+      bit_vec_visited = true;
+      REQUIRE(bit_vec.bit_width() == 8);
+    }
+  } visitor;
+  smt_bit_vector_sortt{8}.accept(visitor);
+  REQUIRE_FALSE(visitor.bool_visited);
+  REQUIRE(visitor.bit_vec_visited);
+}
+
+TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
+{
+  const smt_bool_sortt bool_sort1;
+  CHECK(bool_sort1 == bool_sort1);
+  const smt_bool_sortt bool_sort2;
+  CHECK(bool_sort1 == bool_sort2);
+  const smt_bit_vector_sortt bit_vector8{8};
+  CHECK(bit_vector8 == bit_vector8);
+  CHECK(bit_vector8 != bool_sort1);
+  const smt_bit_vector_sortt bit_vector16{16};
+  CHECK(bit_vector8 != bit_vector16);
+}
diff --git a/unit/solvers/smt2_incremental/smt_terms.cpp b/unit/solvers/smt2_incremental/smt_terms.cpp
new file mode 100644
index 00000000000..5dd48356d89
--- /dev/null
+++ b/unit/solvers/smt2_incremental/smt_terms.cpp
@@ -0,0 +1,203 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+#include <util/mp_arith.h>
+
+#include <type_traits>
+
+TEST_CASE("Test smt_termt.pretty is accessible.", "[core][smt2_incremental]")
+{
+  const smt_termt bool_term{smt_bool_literal_termt{true}};
+  REQUIRE(
+    bool_term.pretty(0, 0) ==
+    "smt_bool_literal_term\n"
+    "  * type: smt_bool_sort\n"
+    "  * value: 1");
+}
+
+TEST_CASE(
+  "Test smt_bool_literal_termt has bool sort.",
+  "[core][smt2_incremental]")
+{
+  REQUIRE(smt_bool_literal_termt{true}.get_sort() == smt_bool_sortt{});
+}
+
+TEST_CASE(
+  "Test smt_bool_literal_termt value getter.",
+  "[core][smt2_incremental]")
+{
+  REQUIRE(smt_bool_literal_termt{true}.value());
+  REQUIRE_FALSE(smt_bool_literal_termt{false}.value());
+}
+
+TEST_CASE("smt_not_termt sort.", "[core][smt2_incremental]")
+{
+  REQUIRE(
+    smt_not_termt{smt_bool_literal_termt{true}}.get_sort() == smt_bool_sortt{});
+}
+
+TEST_CASE("smt_not_termt operand getter.", "[core][smt2_incremental]")
+{
+  const smt_bool_literal_termt bool_term{true};
+  const smt_not_termt not_term{bool_term};
+  REQUIRE(not_term.operand() == bool_term);
+}
+
+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{}});
+}
+
+TEST_CASE("smt_identifier_termt getters.", "[core][smt2_incremental]")
+{
+  const smt_identifier_termt identifier{"foo", smt_bool_sortt{}};
+  CHECK(identifier.identifier() == "foo");
+  CHECK(identifier.get_sort() == smt_bool_sortt{});
+}
+
+TEST_CASE("smt_bit_vector_constant_termt getters.", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt bit_vector{32, 8};
+  CHECK(bit_vector.value() == 32);
+  CHECK(bit_vector.get_sort() == smt_bit_vector_sortt{8});
+}
+
+TEST_CASE("smt_termt equality.", "[core][smt2_incremental]")
+{
+  smt_termt false_term = smt_bool_literal_termt{false};
+  CHECK(false_term == false_term);
+  CHECK(false_term == smt_bool_literal_termt{false});
+  smt_termt true_term = smt_bool_literal_termt{true};
+  CHECK_FALSE(false_term == true_term);
+  CHECK(
+    smt_bit_vector_constant_termt{42, 8} !=
+    smt_bit_vector_constant_termt{12, 8});
+  smt_termt not_false = smt_not_termt{smt_bool_literal_termt{false}};
+  smt_termt not_true = smt_not_termt{smt_bool_literal_termt{true}};
+  CHECK_FALSE(not_false == true_term);
+  CHECK_FALSE(not_false == not_true);
+  CHECK(not_false == smt_not_termt{smt_bool_literal_termt{false}});
+}
+
+template <typename expected_termt>
+class term_visit_type_checkert final : public smt_term_const_downcast_visitort
+{
+public:
+  bool expected_term_visited = false;
+  bool unexpected_term_visited = false;
+
+  void visit(const smt_bool_literal_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_bool_literal_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_not_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_not_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_identifier_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_identifier_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_bit_vector_constant_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_bit_vector_constant_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_function_application_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_function_application_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+};
+
+template <typename term_typet>
+term_typet make_test_term();
+
+template <>
+smt_bool_literal_termt make_test_term<smt_bool_literal_termt>()
+{
+  return smt_bool_literal_termt{false};
+}
+
+template <>
+smt_not_termt make_test_term<smt_not_termt>()
+{
+  return smt_not_termt{smt_bool_literal_termt{false}};
+}
+
+template <>
+smt_identifier_termt make_test_term<smt_identifier_termt>()
+{
+  return smt_identifier_termt{"foo", smt_bool_sortt{}};
+}
+
+template <>
+smt_bit_vector_constant_termt make_test_term<smt_bit_vector_constant_termt>()
+{
+  return smt_bit_vector_constant_termt{0, 32};
+}
+
+template <>
+smt_function_application_termt make_test_term<smt_function_application_termt>()
+{
+  return smt_function_application_termt{
+    smt_identifier_termt{"bar", smt_bool_sortt{}}, {}};
+}
+
+TEMPLATE_TEST_CASE(
+  "smt_termt::accept(visitor)",
+  "[core][smt2_incremental]",
+  smt_bool_literal_termt,
+  smt_not_termt,
+  smt_identifier_termt,
+  smt_bit_vector_constant_termt,
+  smt_function_application_termt)
+{
+  term_visit_type_checkert<TestType> checker;
+  make_test_term<TestType>().accept(checker);
+  CHECK(checker.expected_term_visited);
+  CHECK_FALSE(checker.unexpected_term_visited);
+}