diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 9fbafd0b4ac..02fc6453e16 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -160,6 +160,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
       strings/array_pool.cpp \
+      strings/equation_symbol_mapping.cpp \
       strings/string_builtin_function.cpp \
       strings/string_refinement.cpp \
       strings/string_refinement_util.cpp \
diff --git a/src/solvers/strings/equation_symbol_mapping.cpp b/src/solvers/strings/equation_symbol_mapping.cpp
new file mode 100644
index 00000000000..9f72a64d604
--- /dev/null
+++ b/src/solvers/strings/equation_symbol_mapping.cpp
@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: String solver
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "equation_symbol_mapping.h"
+
+void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
+{
+  equations_containing[expr].push_back(i);
+  strings_in_equation[i].push_back(expr);
+}
+
+std::vector<exprt>
+equation_symbol_mappingt::find_expressions(const std::size_t i)
+{
+  return strings_in_equation[i];
+}
+
+std::vector<std::size_t>
+equation_symbol_mappingt::find_equations(const exprt &expr)
+{
+  return equations_containing[expr];
+}
diff --git a/src/solvers/strings/equation_symbol_mapping.h b/src/solvers/strings/equation_symbol_mapping.h
new file mode 100644
index 00000000000..55e8c15e86f
--- /dev/null
+++ b/src/solvers/strings/equation_symbol_mapping.h
@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module: String solver
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
+#define CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
+
+#include <map>
+#include <unordered_map>
+
+#include <util/expr.h>
+
+/// Maps equation to expressions contained in them and conversely expressions to
+/// equations that contain them. This can be used on a subset of expressions
+/// which interests us, in particular strings. Equations are identified by an
+/// index of type `std::size_t` for more efficient insertion and lookup.
+class equation_symbol_mappingt
+{
+public:
+  /// Record the fact that equation `i` contains expression `expr`
+  void add(const std::size_t i, const exprt &expr);
+
+  /// \param i: index corresponding to an equation
+  /// \return vector of expressions contained in the equation with the given
+  ///   index `i`
+  std::vector<exprt> find_expressions(const std::size_t i);
+
+  /// \param expr: an expression
+  /// \return vector of equations containing the given expression `expr`
+  std::vector<std::size_t> find_equations(const exprt &expr);
+
+private:
+  /// Record index of the equations that contain a given expression
+  std::map<exprt, std::vector<std::size_t>> equations_containing;
+  /// Record expressions that are contained in the equation with the given index
+  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
+};
+
+#endif // CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 7f69b14b3a1..fd2db24e300 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -18,7 +18,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 ///   Ghosh.
 
 #include "string_refinement.h"
-#include "string_constraint_instantiation.h"
 
 #include <iomanip>
 #include <numeric>
@@ -30,6 +29,9 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/magic.h>
 #include <util/simplify_expr.h>
 
+#include "equation_symbol_mapping.h"
+#include "string_constraint_instantiation.h"
+
 static bool is_valid_string_constraint(
   messaget::mstreamt &stream,
   const namespacet &ns,
diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp
index e05b909e44b..e0d366b6d41 100644
--- a/src/solvers/strings/string_refinement_util.cpp
+++ b/src/solvers/strings/string_refinement_util.cpp
@@ -183,24 +183,6 @@ array_exprt interval_sparse_arrayt::concretize(
   return array;
 }
 
-void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
-{
-  equations_containing[expr].push_back(i);
-  strings_in_equation[i].push_back(expr);
-}
-
-std::vector<exprt>
-equation_symbol_mappingt::find_expressions(const std::size_t i)
-{
-  return strings_in_equation[i];
-}
-
-std::vector<std::size_t>
-equation_symbol_mappingt::find_equations(const exprt &expr)
-{
-  return equations_containing[expr];
-}
-
 /// Construct a string_builtin_functiont object from a function application
 /// \return a unique pointer to the created object
 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
diff --git a/src/solvers/strings/string_refinement_util.h b/src/solvers/strings/string_refinement_util.h
index 89cf37d81b5..678ebc34a99 100644
--- a/src/solvers/strings/string_refinement_util.h
+++ b/src/solvers/strings/string_refinement_util.h
@@ -132,32 +132,6 @@ class interval_sparse_arrayt final : public sparse_arrayt
   }
 };
 
-/// Maps equation to expressions contained in them and conversely expressions to
-/// equations that contain them. This can be used on a subset of expressions
-/// which interests us, in particular strings. Equations are identified by an
-/// index of type `std::size_t` for more efficient insertion and lookup.
-class equation_symbol_mappingt
-{
-public:
-  /// Record the fact that equation `i` contains expression `expr`
-  void add(const std::size_t i, const exprt &expr);
-
-  /// \param i: index corresponding to an equation
-  /// \return vector of expressions contained in the equation with the given
-  ///   index `i`
-  std::vector<exprt> find_expressions(const std::size_t i);
-
-  /// \param expr: an expression
-  /// \return vector of equations containing the given expression `expr`
-  std::vector<std::size_t> find_equations(const exprt &expr);
-
-private:
-  /// Record index of the equations that contain a given expression
-  std::map<exprt, std::vector<std::size_t>> equations_containing;
-  /// Record expressions that are contained in the equation with the given index
-  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
-};
-
 /// Keep track of dependencies between strings.
 /// Each string points to the builtin_function calls on which it depends.
 /// Each builtin_function points to the strings on which the result depends.