diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 81aed1cec6a..d44caf4c234 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -198,6 +198,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
       smt2_incremental/smt_core_theory.cpp \
+      smt2_incremental/smt_index.cpp \
       smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_response_validation.cpp \
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
index 50a8a70f677..c529bf82d37 100644
--- a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
+++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -4,6 +4,37 @@
 
 #include <util/invariant.h>
 
+const char *smt_bit_vector_theoryt::extractt::identifier()
+{
+  return "extract";
+}
+
+smt_sortt
+smt_bit_vector_theoryt::extractt::return_sort(const smt_termt &operand) const
+{
+  return smt_bit_vector_sortt{i - j + 1};
+}
+
+std::vector<smt_indext> smt_bit_vector_theoryt::extractt::indices() const
+{
+  return {smt_numeral_indext{i}, smt_numeral_indext{j}};
+}
+
+void smt_bit_vector_theoryt::extractt::validate(const smt_termt &operand) const
+{
+  PRECONDITION(i >= j);
+  const auto bit_vector_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
+  PRECONDITION(bit_vector_sort);
+  PRECONDITION(i < bit_vector_sort->bit_width());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::extractt>
+smt_bit_vector_theoryt::extract(std::size_t i, std::size_t j)
+{
+  PRECONDITION(i >= j);
+  return smt_function_application_termt::factoryt<extractt>(i, j);
+}
+
 static void validate_bit_vector_operator_arguments(
   const smt_termt &left,
   const smt_termt &right)
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.h b/src/solvers/smt2_incremental/smt_bit_vector_theory.h
index b90c5e0ab67..07c4b45188a 100644
--- a/src/solvers/smt2_incremental/smt_bit_vector_theory.h
+++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.h
@@ -8,6 +8,18 @@
 class smt_bit_vector_theoryt
 {
 public:
+  struct extractt final
+  {
+    std::size_t i;
+    std::size_t j;
+    static const char *identifier();
+    smt_sortt return_sort(const smt_termt &operand) const;
+    std::vector<smt_indext> indices() const;
+    void validate(const smt_termt &operand) const;
+  };
+  static smt_function_application_termt::factoryt<extractt>
+  extract(std::size_t i, std::size_t j);
+
   // Relational operator class declarations
   struct unsigned_less_thant final
   {
diff --git a/src/solvers/smt2_incremental/smt_index.cpp b/src/solvers/smt2_incremental/smt_index.cpp
new file mode 100644
index 00000000000..8912dc22da3
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_index.cpp
@@ -0,0 +1,65 @@
+// Author: Diffblue Ltd.
+
+#include "smt_index.h"
+
+// Define the irep_idts for kinds of index.
+const irep_idt ID_smt_numeral_index{"smt_numeral_index"};
+const irep_idt ID_smt_symbol_index{"smt_symbol_index"};
+
+bool smt_indext::operator==(const smt_indext &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_indext::operator!=(const smt_indext &other) const
+{
+  return !(*this == other);
+}
+
+template <>
+const smt_numeral_indext *smt_indext::cast<smt_numeral_indext>() const &
+{
+  return id() == ID_smt_numeral_index
+           ? static_cast<const smt_numeral_indext *>(this)
+           : nullptr;
+}
+
+template <>
+const smt_symbol_indext *smt_indext::cast<smt_symbol_indext>() const &
+{
+  return id() == ID_smt_symbol_index
+           ? static_cast<const smt_symbol_indext *>(this)
+           : nullptr;
+}
+
+void smt_indext::accept(smt_index_const_downcast_visitort &visitor) const
+{
+  if(const auto numeral = this->cast<smt_numeral_indext>())
+    return visitor.visit(*numeral);
+  if(const auto symbol = this->cast<smt_symbol_indext>())
+    return visitor.visit(*symbol);
+  UNREACHABLE;
+}
+
+smt_numeral_indext::smt_numeral_indext(std::size_t value)
+  : smt_indext{ID_smt_numeral_index}
+{
+  set_size_t(ID_value, value);
+}
+
+std::size_t smt_numeral_indext::value() const
+{
+  return get_size_t(ID_value);
+}
+
+smt_symbol_indext::smt_symbol_indext(irep_idt identifier)
+  : smt_indext{ID_smt_symbol_index}
+{
+  PRECONDITION(!identifier.empty());
+  set(ID_identifier, identifier);
+}
+
+irep_idt smt_symbol_indext::identifier() const
+{
+  return get(ID_identifier);
+}
diff --git a/src/solvers/smt2_incremental/smt_index.h b/src/solvers/smt2_incremental/smt_index.h
new file mode 100644
index 00000000000..252d904feb8
--- /dev/null
+++ b/src/solvers/smt2_incremental/smt_index.h
@@ -0,0 +1,90 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
+
+#include <util/irep.h>
+
+class smt_index_const_downcast_visitort;
+
+/// \brief
+/// For implementation of indexed identifiers. See SMT-LIB Standard Version 2.6
+/// section 3.3.
+class smt_indext : protected irept
+{
+public:
+  // smt_indext does not support the notion of an empty / null state. Use
+  // optionalt<smt_indext> instead if an empty index is required.
+  smt_indext() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_indext &) const;
+  bool operator!=(const smt_indext &) const;
+
+  template <typename sub_classt>
+  const sub_classt *cast() const &;
+
+  void accept(smt_index_const_downcast_visitort &) const;
+
+  /// \brief Class for adding the ability to up and down cast smt_indext 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_indext index);
+    static const smt_indext &downcast(const irept &);
+  };
+
+protected:
+  using irept::irept;
+};
+
+template <typename derivedt>
+smt_indext::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_indext::storert<derivedt>::upcast(smt_indext index)
+{
+  return static_cast<irept &&>(std::move(index));
+}
+
+template <typename derivedt>
+const smt_indext &smt_indext::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_indext &>(irep);
+}
+
+class smt_numeral_indext : public smt_indext
+{
+public:
+  explicit smt_numeral_indext(std::size_t value);
+  std::size_t value() const;
+};
+
+class smt_symbol_indext : public smt_indext
+{
+public:
+  explicit smt_symbol_indext(irep_idt identifier);
+  irep_idt identifier() const;
+};
+
+class smt_index_const_downcast_visitort
+{
+public:
+  virtual void visit(const smt_numeral_indext &) = 0;
+  virtual void visit(const smt_symbol_indext &) = 0;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp
index 11855a2eed0..e3022cb3160 100644
--- a/src/solvers/smt2_incremental/smt_terms.cpp
+++ b/src/solvers/smt2_incremental/smt_terms.cpp
@@ -56,7 +56,10 @@ static bool is_valid_smt_identifier(irep_idt identifier)
   return std::regex_match(id2string(identifier), valid);
 }
 
-smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
+smt_identifier_termt::smt_identifier_termt(
+  irep_idt identifier,
+  smt_sortt sort,
+  std::vector<smt_indext> indices)
   : smt_termt(ID_smt_identifier_term, std::move(sort))
 {
   // The below invariant exists as a sanity check that the string being used for
@@ -67,6 +70,11 @@ smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
     is_valid_smt_identifier(identifier),
     R"(Identifiers may not contain | characters.)");
   set(ID_identifier, identifier);
+  for(auto &index : indices)
+  {
+    get_sub().push_back(
+      smt_indext::storert<smt_identifier_termt>::upcast(std::move(index)));
+  }
 }
 
 irep_idt smt_identifier_termt::identifier() const
@@ -74,6 +82,15 @@ irep_idt smt_identifier_termt::identifier() const
   return get(ID_identifier);
 }
 
+std::vector<std::reference_wrapper<const smt_indext>>
+smt_identifier_termt::indices() const
+{
+  return make_range(get_sub()).map([](const irept &index) {
+    return std::cref(
+      smt_indext::storert<smt_identifier_termt>::downcast(index));
+  });
+}
+
 smt_bit_vector_constant_termt::smt_bit_vector_constant_termt(
   const mp_integer &value,
   smt_bit_vector_sortt sort)
diff --git a/src/solvers/smt2_incremental/smt_terms.h b/src/solvers/smt2_incremental/smt_terms.h
index 0925c598c4a..b8cfc4b4fa8 100644
--- a/src/solvers/smt2_incremental/smt_terms.h
+++ b/src/solvers/smt2_incremental/smt_terms.h
@@ -3,10 +3,14 @@
 #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 <solvers/smt2_incremental/smt_index.h>
+#include <solvers/smt2_incremental/smt_sorts.h>
+#include <solvers/smt2_incremental/type_traits.h>
+
 #include <functional>
+#include <utility>
 
 class BigInt;
 using mp_integer = BigInt;
@@ -77,7 +81,14 @@ class smt_bool_literal_termt : public smt_termt
 
 /// Stores identifiers in unescaped and unquoted form. Any escaping or quoting
 /// required should be performed during printing.
-class smt_identifier_termt : public smt_termt
+/// \details
+/// The SMT-LIB standard Version 2.6 refers to "indexed" identifiers which have
+/// 1 or more indices and "simple" identifiers which have no indicies. The
+/// internal `smt_identifier_termt` class is used for both kinds of identifier
+/// which are distinguished based on whether the collection of `indices` is
+/// empty or not.
+class smt_identifier_termt : public smt_termt,
+                             private smt_indext::storert<smt_identifier_termt>
 {
 public:
   /// \brief Constructs an identifier term with the given \p identifier and
@@ -91,8 +102,14 @@ class smt_identifier_termt : public smt_termt
   /// \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);
+  /// \param indices: This should be collection of indices for an indexed
+  ///   identifier, or an empty collection for simple (non-indexed) identifiers.
+  smt_identifier_termt(
+    irep_idt identifier,
+    smt_sortt sort,
+    std::vector<smt_indext> indices = {});
   irep_idt identifier() const;
+  std::vector<std::reference_wrapper<const smt_indext>> indices() const;
 };
 
 class smt_bit_vector_constant_termt : public smt_termt
@@ -121,6 +138,44 @@ class smt_function_application_termt : public smt_termt
     smt_identifier_termt function_identifier,
     std::vector<smt_termt> arguments);
 
+  // This is used to detect if \p functiont has an `indicies` member function.
+  // It will resolve to std::true_type if it does or std::false type otherwise.
+  template <class functiont, class = void>
+  struct has_indicest : std::false_type
+  {
+  };
+
+  template <class functiont>
+  struct has_indicest<
+    functiont,
+    void_t<decltype(std::declval<functiont>().indices())>> : std::true_type
+  {
+  };
+
+  /// Overload for when \p functiont does not have indices.
+  template <class functiont>
+  static std::vector<smt_indext>
+  indices(const functiont &function, const std::false_type &has_indices)
+  {
+    return {};
+  }
+
+  /// Overload for when \p functiont has indices member function.
+  template <class functiont>
+  static std::vector<smt_indext>
+  indices(const functiont &function, const std::true_type &has_indices)
+  {
+    return function.indices();
+  }
+
+  /// Returns `function.indices` if `functiont` has an `indices` member function
+  /// or returns an empty collection otherwise.
+  template <class functiont>
+  static std::vector<smt_indext> indices(const functiont &function)
+  {
+    return indices(function, has_indicest<functiont>{});
+  }
+
 public:
   const smt_identifier_termt &function_identifier() const;
   std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
@@ -133,7 +188,7 @@ class smt_function_application_termt : public smt_termt
 
   public:
     template <typename... function_type_argument_typest>
-    explicit factoryt(function_type_argument_typest &&... arguments)
+    explicit factoryt(function_type_argument_typest &&... arguments) noexcept
       : function{std::forward<function_type_argument_typest>(arguments)...}
     {
     }
@@ -145,7 +200,8 @@ class smt_function_application_termt : public smt_termt
       function.validate(arguments...);
       auto return_sort = function.return_sort(arguments...);
       return smt_function_application_termt{
-        smt_identifier_termt{function.identifier(), std::move(return_sort)},
+        smt_identifier_termt{
+          function.identifier(), std::move(return_sort), indices(function)},
         {std::forward<argument_typest>(arguments)...}};
     }
   };
diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
index 54634fe4d37..8a7c8cc70c1 100644
--- a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
+++ b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
@@ -1,15 +1,15 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <util/range.h>
+#include <util/string_utils.h>
 
 #include <solvers/smt2/smt2_conv.h>
 #include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_index.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 <solvers/smt2_incremental/smt_to_smt2_string.h>
 
 #include <functional>
 #include <iostream>
@@ -17,6 +17,46 @@
 #include <stack>
 #include <string>
 
+static std::string escape_identifier(const irep_idt &identifier)
+{
+  return std::string{"|"} + smt2_convt::convert_identifier(identifier) + "|";
+}
+
+class smt_index_output_visitort : public smt_index_const_downcast_visitort
+{
+protected:
+  std::ostream &os;
+
+public:
+  explicit smt_index_output_visitort(std::ostream &os) : os(os)
+  {
+  }
+
+  void visit(const smt_numeral_indext &numeral) override
+  {
+    os << numeral.value();
+  }
+
+  void visit(const smt_symbol_indext &symbol) override
+  {
+    os << escape_identifier(symbol.identifier());
+  }
+};
+
+std::ostream &operator<<(std::ostream &os, const smt_indext &index)
+{
+  smt_index_output_visitort visitor{os};
+  index.accept(visitor);
+  return os;
+}
+
+std::string smt_to_smt2_string(const smt_indext &index)
+{
+  std::stringstream ss;
+  ss << index;
+  return ss.str();
+}
+
 class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
 {
 protected:
@@ -73,10 +113,12 @@ class smt_term_to_string_convertert : private smt_term_const_downcast_visitort
   std::stack<output_functiont> output_stack;
 
   static output_functiont make_output_function(const std::string &output);
+  static output_functiont make_output_function(const smt_indext &output);
   static output_functiont make_output_function(const smt_sortt &output);
   output_functiont make_output_function(const smt_termt &output);
+  template <typename elementt>
   output_functiont make_output_function(
-    const std::vector<std::reference_wrapper<const smt_termt>> &output);
+    const std::vector<std::reference_wrapper<const elementt>> &output);
 
   /// \brief Single argument version of `push_outputs`.
   template <typename outputt>
@@ -121,6 +163,12 @@ smt_term_to_string_convertert::make_output_function(const std::string &output)
   return [output](std::ostream &os) { os << output; };
 }
 
+smt_term_to_string_convertert::output_functiont
+smt_term_to_string_convertert::make_output_function(const smt_indext &output)
+{
+  return [=](std::ostream &os) { os << output; };
+}
+
 smt_term_to_string_convertert::output_functiont
 smt_term_to_string_convertert::make_output_function(const smt_sortt &output)
 {
@@ -133,9 +181,10 @@ smt_term_to_string_convertert::make_output_function(const smt_termt &output)
   return [=](std::ostream &os) { output.accept(*this); };
 }
 
+template <typename elementt>
 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)
+  const std::vector<std::reference_wrapper<const elementt>> &outputs)
 {
   return [=](std::ostream &os) {
     for(const auto &output : make_range(outputs.rbegin(), outputs.rend()))
@@ -173,8 +222,16 @@ void smt_term_to_string_convertert::visit(
 void smt_term_to_string_convertert::visit(
   const smt_identifier_termt &identifier_term)
 {
-  push_outputs(
-    "|", smt2_convt::convert_identifier(identifier_term.identifier()), "|");
+  auto indices = identifier_term.indices();
+  auto escaped_identifier = escape_identifier(identifier_term.identifier());
+  if(indices.empty())
+  {
+    push_outputs(std::move(escaped_identifier));
+  }
+  else
+  {
+    push_outputs("(_ ", std::move(escaped_identifier), std::move(indices), ")");
+  }
 }
 
 void smt_term_to_string_convertert::visit(
diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.h b/src/solvers/smt2_incremental/smt_to_smt2_string.h
index c8e78aa5255..40526046b4e 100644
--- a/src/solvers/smt2_incremental/smt_to_smt2_string.h
+++ b/src/solvers/smt2_incremental/smt_to_smt2_string.h
@@ -8,6 +8,7 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H
 
+class smt_indext;
 class smt_sortt;
 class smt_termt;
 class smt_optiont;
@@ -17,12 +18,14 @@ class smt_logict;
 #include <iosfwd>
 #include <string>
 
+std::ostream &operator<<(std::ostream &os, const smt_indext &index);
 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_smt2_string(const smt_indext &index);
 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);
diff --git a/src/solvers/smt2_incremental/type_traits.h b/src/solvers/smt2_incremental/type_traits.h
new file mode 100644
index 00000000000..ea928e1ddb7
--- /dev/null
+++ b/src/solvers/smt2_incremental/type_traits.h
@@ -0,0 +1,37 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Back ports of utilities available in the `<type_traits>` library for C++14
+/// or C++17 to C++11. These can be replaced with the standard library versions
+/// as and when we upgrade the version CBMC is compiled with.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
+
+#include <type_traits>
+
+namespace detail // NOLINT
+{
+// Implementation detail of `void_t`.
+template <typename... typest>
+struct make_voidt
+{
+  using type = void;
+};
+} // namespace detail
+
+// The below definition is of a back-ported version of the C++17 STL
+// `std::void_t` template. This makes this particular template available when
+// compiling for the C++11 or C++14 standard versions. It will also compile
+// as-is when targeting the C++17 standard. The back-ported version is not added
+// to the `std` namespace as this would be undefined behaviour. However once we
+// permanently move to the new standard the below code should be removed
+// and `std::void_t` should be used directly, to avoid polluting the global
+// namespace. For example -
+//   `void_t<decltype(foo.bar())>`
+// should be updated to -
+//   `std::void_t<decltype(foo.bar())>`
+template <typename... typest>
+using void_t = typename detail::make_voidt<typest...>::type;
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
diff --git a/unit/Makefile b/unit/Makefile
index a27013a2bdf..07e67e1f653 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -106,6 +106,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
        solvers/smt2_incremental/smt_core_theory.cpp \
+       solvers/smt2_incremental/smt_index.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_responses.cpp \
        solvers/smt2_incremental/smt_sorts.cpp \
diff --git a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
index dbfb5d678b7..8166fe29c36 100644
--- a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
+++ b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -7,6 +7,33 @@
 
 #include <util/mp_arith.h>
 
+TEST_CASE("SMT bit vector extract", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt operand{42, 8};
+  const auto extract_4_3 = smt_bit_vector_theoryt::extract(4, 3);
+  SECTION("Valid construction")
+  {
+    const auto extraction = extract_4_3(operand);
+    const auto expected_return_sort = smt_bit_vector_sortt{2};
+    REQUIRE(
+      extraction.function_identifier() ==
+      smt_identifier_termt(
+        "extract",
+        expected_return_sort,
+        {smt_numeral_indext{4}, smt_numeral_indext{3}}));
+    REQUIRE(extraction.get_sort() == expected_return_sort);
+    REQUIRE(extraction.arguments().size() == 1);
+    REQUIRE(extraction.arguments()[0].get() == operand);
+  }
+  SECTION("Invalid constructions")
+  {
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::extract(3, 4));
+    REQUIRE_THROWS(extract_4_3(smt_bool_literal_termt{true}));
+    REQUIRE_THROWS(extract_4_3(smt_bit_vector_constant_termt{8, 4}));
+  }
+}
+
 TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
 {
   const smt_bit_vector_constant_termt two{2, 8};
diff --git a/unit/solvers/smt2_incremental/smt_index.cpp b/unit/solvers/smt2_incremental/smt_index.cpp
new file mode 100644
index 00000000000..8b6fb87cbdb
--- /dev/null
+++ b/unit/solvers/smt2_incremental/smt_index.cpp
@@ -0,0 +1,76 @@
+// Author: Diffblue Ltd.
+
+#include <util/optional.h>
+
+#include <solvers/smt2_incremental/smt_index.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Test smt_indext.pretty is accessible.", "[core][smt2_incremental]")
+{
+  const smt_indext index = smt_numeral_indext{42};
+  REQUIRE_FALSE(index.pretty().empty());
+}
+
+TEST_CASE("Test smt_symbol_index construction", "[core][smt2_incremental]")
+{
+  const cbmc_invariants_should_throwt invariants_throw;
+  CHECK_NOTHROW(smt_symbol_indext{"foo"});
+  CHECK_THROWS(smt_symbol_indext{""});
+}
+
+TEST_CASE("Test smt_index getters", "[core][smt2_incremental]")
+{
+  SECTION("Numeral")
+  {
+    REQUIRE(smt_numeral_indext{42}.value() == 42);
+  }
+  SECTION("Symbol")
+  {
+    REQUIRE(smt_symbol_indext{"foo"}.identifier() == "foo");
+  }
+}
+
+TEST_CASE("Visiting smt_indext", "[core][smt2_incremental]")
+{
+  class : public smt_index_const_downcast_visitort
+  {
+  public:
+    optionalt<std::size_t> numeral_visited{};
+    optionalt<irep_idt> symbol_visited{};
+
+    void visit(const smt_numeral_indext &numeral) override
+    {
+      numeral_visited = numeral.value();
+    }
+
+    void visit(const smt_symbol_indext &symbol) override
+    {
+      symbol_visited = symbol.identifier();
+    }
+  } visitor;
+  SECTION("numeral")
+  {
+    smt_numeral_indext{8}.accept(visitor);
+    REQUIRE(visitor.numeral_visited);
+    CHECK(*visitor.numeral_visited == 8);
+    CHECK_FALSE(visitor.symbol_visited);
+  }
+  SECTION("symbol")
+  {
+    smt_symbol_indext{"bar"}.accept(visitor);
+    CHECK_FALSE(visitor.numeral_visited);
+    REQUIRE(visitor.symbol_visited);
+    CHECK(*visitor.symbol_visited == "bar");
+  }
+}
+
+TEST_CASE("smt_index equality", "[core][smt2_incremental]")
+{
+  const smt_symbol_indext foo_index{"foo"};
+  CHECK(foo_index == smt_symbol_indext{"foo"});
+  CHECK(foo_index != smt_symbol_indext{"bar"});
+  const smt_numeral_indext index_42{42};
+  CHECK(index_42 == smt_numeral_indext{42});
+  CHECK(index_42 != smt_numeral_indext{12});
+  CHECK(index_42 != foo_index);
+}
diff --git a/unit/solvers/smt2_incremental/smt_terms.cpp b/unit/solvers/smt2_incremental/smt_terms.cpp
index fdc873b40ad..0405b5fb109 100644
--- a/unit/solvers/smt2_incremental/smt_terms.cpp
+++ b/unit/solvers/smt2_incremental/smt_terms.cpp
@@ -44,9 +44,26 @@ TEST_CASE("smt_identifier_termt construction", "[core][smt2_incremental]")
 
 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{});
+  SECTION("Simple identifier")
+  {
+    const smt_identifier_termt identifier{"foo", smt_bool_sortt{}};
+    CHECK(identifier.identifier() == "foo");
+    CHECK(identifier.get_sort() == smt_bool_sortt{});
+    CHECK(identifier.indices().empty());
+  }
+  SECTION("Indexed identifier")
+  {
+    const smt_symbol_indext baz{"baz"};
+    const smt_numeral_indext index_42{42};
+    const smt_identifier_termt indexed{
+      "bar", smt_bit_vector_sortt{8}, {baz, index_42}};
+    CHECK(indexed.identifier() == "bar");
+    CHECK(indexed.get_sort() == smt_bit_vector_sortt{8});
+    const auto indices = indexed.indices();
+    REQUIRE(indices.size() == 2);
+    CHECK(indices[0].get() == baz);
+    CHECK(indices[1].get() == index_42);
+  }
 }
 
 TEST_CASE("smt_bit_vector_constant_termt getters.", "[core][smt2_incremental]")
diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
index 1d4800c34ba..4f1475e922f 100644
--- a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
+++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
@@ -1,15 +1,21 @@
 // Author: Diffblue Ltd.
 
-#include <testing-utils/use_catch.h>
+#include <util/mp_arith.h>
 
+#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.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_smt2_string.h>
+#include <testing-utils/use_catch.h>
 
-#include <util/mp_arith.h>
+TEST_CASE("Test smt_indext to string conversion", "[core][smt2_incremental]")
+{
+  CHECK(smt_to_smt2_string(smt_symbol_indext{"green"}) == "|green|");
+  CHECK(smt_to_smt2_string(smt_numeral_indext{42}) == "42");
+}
 
 TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
 {
@@ -24,6 +30,15 @@ TEST_CASE(
   CHECK(smt_to_smt2_string(smt_bit_vector_constant_termt{0, 8}) == "(_ bv0 8)");
 }
 
+TEST_CASE(
+  "Test smt_bit_vector extract to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_smt2_string(smt_bit_vector_theoryt::extract(7, 3)(
+      smt_bit_vector_constant_termt{0, 8})) == "((_ |extract| 7 3) (_ bv0 8))");
+}
+
 TEST_CASE(
   "Test smt_bool_literal_termt to string conversion",
   "[core][smt2_incremental]")
@@ -36,12 +51,24 @@ TEST_CASE(
   "Test smt_identifier_termt to string conversion",
   "[core][smt2_incremental]")
 {
-  CHECK(
-    smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) ==
-    "|abc|");
-  CHECK(
-    smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) ==
-    "|&92;|");
+  SECTION("Simple identifiers")
+  {
+    CHECK(
+      smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) ==
+      "|abc|");
+    CHECK(
+      smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) ==
+      "|&92;|");
+  }
+  SECTION("Indexed identifier")
+  {
+    CHECK(
+      smt_to_smt2_string(smt_identifier_termt{
+        "foo",
+        smt_bool_sortt{},
+        {smt_symbol_indext{"bar"}, smt_numeral_indext{42}}}) ==
+      "(_ |foo| |bar| 42)");
+  }
 }
 
 TEST_CASE(