diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
index 094d6850c93..9cc6ecef058 100644
--- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -202,7 +202,7 @@ SCENARIO("instantiate_not_contains",
 
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
-    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
 
     std::accumulate(
       constraints.universal.begin(),
@@ -218,12 +218,12 @@ SCENARIO("instantiate_not_contains",
       constraints.not_contains.end(),
       axioms,
       [&](const std::string &accu, string_not_contains_constraintt sc) {
-        simplify(sc, ns);
+        simplify(sc.premise, ns);
+        simplify(sc.s0, ns);
+        simplify(sc.s1, ns);
         witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
         nc_axioms.push_back(sc);
-        std::string s;
-        java_lang->from_expr(sc, s, ns);
-        return accu + s + "\n\n";
+        return accu + to_string(sc) + "\n\n";
       });
 
     axioms = std::accumulate(
@@ -282,26 +282,23 @@ SCENARIO("instantiate_not_contains",
     //   { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y]
     // )
     // which is vacuously true.
-    string_not_contains_constraintt vacuous(
-      from_integer(0),
-      from_integer(0),
-      true_exprt(),
-      from_integer(0),
-      from_integer(1),
-      a_array,
-      a_array);
+    const string_not_contains_constraintt vacuous = {from_integer(0),
+                                                     from_integer(0),
+                                                     true_exprt(),
+                                                     from_integer(0),
+                                                     from_integer(1),
+                                                     a_array,
+                                                     a_array};
 
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    std::string s;
-    java_lang->from_expr(vacuous, s, ns);
-    INFO(s + "\n\n");
+    INFO(to_string(vacuous) + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -337,26 +334,23 @@ SCENARIO("instantiate_not_contains",
     //   { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y]
     // )
     // which is false.
-    string_not_contains_constraintt trivial(
-      from_integer(0),
-      from_integer(1),
-      true_exprt(),
-      from_integer(0),
-      from_integer(0),
-      a_array,
-      b_array);
+    const string_not_contains_constraintt trivial = {from_integer(0),
+                                                     from_integer(1),
+                                                     true_exprt(),
+                                                     from_integer(0),
+                                                     from_integer(0),
+                                                     a_array,
+                                                     b_array};
 
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet ns(symtab);
     string_constraint_generatort generator(ns);
-    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    std::string s;
-    java_lang->from_expr(trivial, s, ns);
-    INFO(s + "\n\n");
+    INFO(to_string(trivial) + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -393,26 +387,23 @@ SCENARIO("instantiate_not_contains",
     //   { .=1, .={ (char)'a' } }[x+y] != { .=0, .={ } }[y]
     // )
     // which is false.
-    string_not_contains_constraintt trivial(
-      from_integer(0),
-      from_integer(1),
-      true_exprt(),
-      from_integer(0),
-      from_integer(0),
-      a_array,
-      empty_array);
+    const string_not_contains_constraintt trivial = {from_integer(0),
+                                                     from_integer(1),
+                                                     true_exprt(),
+                                                     from_integer(0),
+                                                     from_integer(0),
+                                                     a_array,
+                                                     empty_array};
 
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    std::string s;
-    java_lang->from_expr(trivial, s, ns);
-    INFO(s + "\n\n");
+    INFO(to_string(trivial) + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -451,27 +442,24 @@ SCENARIO("instantiate_not_contains",
     //   { .=2, .={ (char)'a', (char)'b'}[y]
     // )
     // which is false (for x = 0).
-    string_not_contains_constraintt trivial(
-      from_integer(0),
-      from_integer(2),
-      true_exprt(),
-      from_integer(0),
-      from_integer(2),
-      ab_array,
-      ab_array);
+    const string_not_contains_constraintt trivial = {from_integer(0),
+                                                     from_integer(2),
+                                                     true_exprt(),
+                                                     from_integer(0),
+                                                     from_integer(2),
+                                                     ab_array,
+                                                     ab_array};
 
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
 
     string_constraint_generatort generator(ns);
-    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    std::string s;
-    java_lang->from_expr(trivial, s, ns);
-    INFO(s + "\n\n");
+    INFO(to_string(trivial) + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -508,26 +496,23 @@ SCENARIO("instantiate_not_contains",
     //   { .=2, .={ (char)'a', (char)'b'}[y]
     // )
     // which is true.
-    string_not_contains_constraintt trivial(
-      from_integer(0),
-      from_integer(2),
-      true_exprt(),
-      from_integer(0),
-      from_integer(2),
-      ab_array,
-      cd_array);
+    const string_not_contains_constraintt trivial = {from_integer(0),
+                                                     from_integer(2),
+                                                     true_exprt(),
+                                                     from_integer(0),
+                                                     from_integer(2),
+                                                     ab_array,
+                                                     cd_array};
 
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
     string_constraint_generatort generator(ns);
-    std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
+    std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    std::string s;
-    java_lang->from_expr(trivial, s, ns);
-    INFO(s + "\n\n");
+    INFO(to_string(trivial) + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp
index 5fd34963693..b297a1bddb9 100644
--- a/src/solvers/refinement/string_constraint.cpp
+++ b/src/solvers/refinement/string_constraint.cpp
@@ -46,3 +46,43 @@ string_constraintt::string_constraintt(
     "String constraints must have non-negative upper bound.\n" +
       upper_bound.pretty());
 }
+
+/// Used for debug printing.
+/// \param [in] expr: constraint to render
+/// \return rendered string
+std::string to_string(const string_not_contains_constraintt &expr)
+{
+  std::ostringstream out;
+  out << "forall x in [" << format(expr.univ_lower_bound) << ", "
+      << format(expr.univ_upper_bound) << "). " << format(expr.premise)
+      << " => ("
+      << "exists y in [" << format(expr.exists_lower_bound) << ", "
+      << format(expr.exists_upper_bound) << "). " << format(expr.s0)
+      << "[x+y] != " << format(expr.s1) << "[y])";
+  return out.str();
+}
+
+void replace(
+  const union_find_replacet &replace_map,
+  string_not_contains_constraintt &constraint)
+{
+  replace_map.replace_expr(constraint.univ_lower_bound);
+  replace_map.replace_expr(constraint.univ_upper_bound);
+  replace_map.replace_expr(constraint.premise);
+  replace_map.replace_expr(constraint.exists_lower_bound);
+  replace_map.replace_expr(constraint.exists_upper_bound);
+  replace_map.replace_expr(constraint.s0);
+  replace_map.replace_expr(constraint.s1);
+}
+
+bool operator==(
+  const string_not_contains_constraintt &left,
+  const string_not_contains_constraintt &right)
+{
+  return left.univ_upper_bound == right.univ_upper_bound &&
+         left.univ_lower_bound == right.univ_lower_bound &&
+         left.exists_lower_bound == right.exists_lower_bound &&
+         left.exists_upper_bound == right.exists_upper_bound &&
+         left.premise == right.premise && left.s0 == right.s0 &&
+         left.s1 == right.s1;
+}
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index 2786f91e0e8..2b77ca6bb64 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -104,7 +104,7 @@ class string_constraintt final
 };
 
 /// Used for debug printing.
-/// \param [in] expr: constraint to render
+/// \param expr: constraint to render
 /// \return rendered string
 inline std::string to_string(const string_constraintt &expr)
 {
@@ -116,98 +116,50 @@ inline std::string to_string(const string_constraintt &expr)
 }
 
 /// Constraints to encode non containement of strings.
-class string_not_contains_constraintt : public exprt
+/// string_not contains_constraintt are formulas of the form:
+/// ```
+/// forall x in [univ_lower_bound, univ_upper_bound[.
+///   premise(x) =>
+///     exists y in [exists_lower_bound, exists_upper_bound[. s0[x+y] != s1[y]
+/// ```
+struct string_not_contains_constraintt
 {
-public:
-  // string_not contains_constraintt are formula of the form:
-  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
-
-  string_not_contains_constraintt(
-    exprt univ_lower_bound,
-    exprt univ_bound_sup,
-    exprt premise,
-    exprt exists_bound_inf,
-    exprt exists_bound_sup,
-    const array_string_exprt &s0,
-    const array_string_exprt &s1)
-    : exprt(ID_string_not_contains_constraint)
-  {
-    copy_to_operands(univ_lower_bound, univ_bound_sup, premise);
-    copy_to_operands(exists_bound_inf, exists_bound_sup, s0);
-    copy_to_operands(s1);
-  };
-
-  const exprt &univ_lower_bound() const
-  {
-    return op0();
-  }
-
-  const exprt &univ_upper_bound() const
-  {
-    return op1();
-  }
-
-  const exprt &premise() const
-  {
-    return op2();
-  }
+  exprt univ_lower_bound;
+  exprt univ_upper_bound;
+  exprt premise;
+  exprt exists_lower_bound;
+  exprt exists_upper_bound;
+  array_string_exprt s0;
+  array_string_exprt s1;
+};
 
-  const exprt &exists_lower_bound() const
-  {
-    return op3();
-  }
+std::string to_string(const string_not_contains_constraintt &expr);
 
-  const exprt &exists_upper_bound() const
-  {
-    return operands()[4];
-  }
+void replace(
+  const union_find_replacet &replace_map,
+  string_not_contains_constraintt &constraint);
 
-  const array_string_exprt &s0() const
-  {
-    return to_array_string_expr(operands()[5]);
-  }
+bool operator==(
+  const string_not_contains_constraintt &left,
+  const string_not_contains_constraintt &right);
 
-  const array_string_exprt &s1() const
+// NOLINTNEXTLINE [allow specialization within 'std']
+namespace std
+{
+template <>
+// NOLINTNEXTLINE [struct identifier 'hash' does not end in t]
+struct hash<string_not_contains_constraintt>
+{
+  size_t operator()(const string_not_contains_constraintt &constraint) const
   {
-    return to_array_string_expr(operands()[6]);
+    return irep_hash()(constraint.univ_lower_bound) ^
+           irep_hash()(constraint.univ_upper_bound) ^
+           irep_hash()(constraint.exists_lower_bound) ^
+           irep_hash()(constraint.exists_upper_bound) ^
+           irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^
+           irep_hash()(constraint.s1);
   }
 };
-
-/// Used for debug printing.
-/// \param [in] expr: constraint to render
-/// \return rendered string
-inline std::string to_string(const string_not_contains_constraintt &expr)
-{
-  std::ostringstream out;
-  out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
-      << format(expr.univ_upper_bound()) << "). " << format(expr.premise())
-      << " => ("
-      << "exists y in [" << format(expr.exists_lower_bound()) << ", "
-      << format(expr.exists_upper_bound()) << "). " << format(expr.s0())
-      << "[x+y] != " << format(expr.s1()) << "[y])";
-  return out.str();
-}
-
-inline const string_not_contains_constraintt
-&to_string_not_contains_constraint(const exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
-  DATA_INVARIANT(
-    expr.operands().size()==7,
-    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
-      "operands"));
-  return static_cast<const string_not_contains_constraintt &>(expr);
-}
-
-inline string_not_contains_constraintt
-&to_string_not_contains_constraint(exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
-  DATA_INVARIANT(
-    expr.operands().size()==7,
-    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
-      "operands"));
-  return static_cast<string_not_contains_constraintt &>(expr);
 }
 
 #endif
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 7b397490191..48e0366f018 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -142,17 +142,16 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
 
   // string_not contains_constraintt are formulas of the form:
   // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
-  string_not_contains_constraintt a4(
-    from_index,
-    offset,
-    contains,
-    from_integer(0, index_type),
-    needle.length(),
-    haystack,
-    needle);
+  const string_not_contains_constraintt a4 = {from_index,
+                                              offset,
+                                              contains,
+                                              from_integer(0, index_type),
+                                              needle.length(),
+                                              haystack,
+                                              needle};
   constraints.not_contains.push_back(a4);
 
-  string_not_contains_constraintt a5(
+  const string_not_contains_constraintt a5 = {
     from_index,
     plus_exprt( // Add 1 for inclusive upper bound.
       minus_exprt(haystack.length(), needle.length()),
@@ -161,7 +160,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
     from_integer(0, index_type),
     needle.length(),
     haystack,
-    needle);
+    needle};
   constraints.not_contains.push_back(a5);
 
   const implies_exprt a6(
@@ -241,24 +240,24 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
     from_index,
     length_diff);
 
-  string_not_contains_constraintt a4(
+  const string_not_contains_constraintt a4 = {
     plus_exprt(offset, from_integer(1, index_type)),
     plus_exprt(end_index, from_integer(1, index_type)),
     contains,
     from_integer(0, index_type),
     needle.length(),
     haystack,
-    needle);
+    needle};
   constraints.not_contains.push_back(a4);
 
-  string_not_contains_constraintt a5(
+  string_not_contains_constraintt a5 = {
     from_integer(0, index_type),
     plus_exprt(end_index, from_integer(1, index_type)),
     not_exprt(contains),
     from_integer(0, index_type),
     needle.length(),
     haystack,
-    needle);
+    needle};
   constraints.not_contains.push_back(a5);
 
   const implies_exprt a6(
diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp
index 2d495cfee11..fb862631ff2 100644
--- a/src/solvers/refinement/string_constraint_generator_testing.cpp
+++ b/src/solvers/refinement/string_constraint_generator_testing.cpp
@@ -266,14 +266,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_contains(
     implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
   constraints.universal.push_back(a4);
 
-  string_not_contains_constraintt a5(
+  const string_not_contains_constraintt a5 = {
     from_integer(0, index_type),
     plus_exprt(from_integer(1, index_type), length_diff),
     and_exprt(not_exprt(contains), s0.axiom_for_length_ge(s1.length())),
     from_integer(0, index_type),
     s1.length(),
     s0,
-    s1);
+    s1};
   constraints.not_contains.push_back(a5);
 
   return {typecast_exprt(contains, f.type()), std::move(constraints)};
diff --git a/src/solvers/refinement/string_constraint_instantiation.cpp b/src/solvers/refinement/string_constraint_instantiation.cpp
index 38d1384d1b6..965611724f4 100644
--- a/src/solvers/refinement/string_constraint_instantiation.cpp
+++ b/src/solvers/refinement/string_constraint_instantiation.cpp
@@ -21,12 +21,13 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 std::vector<exprt> instantiate_not_contains(
   const string_not_contains_constraintt &axiom,
   const std::set<std::pair<exprt, exprt>> &index_pairs,
-  const std::map<string_not_contains_constraintt, symbol_exprt> &witnesses)
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
+    &witnesses)
 {
   std::vector<exprt> lemmas;
 
-  const array_string_exprt s0 = axiom.s0();
-  const array_string_exprt s1 = axiom.s1();
+  const array_string_exprt s0 = axiom.s0;
+  const array_string_exprt s1 = axiom.s1;
 
   for(const auto &pair : index_pairs)
   {
@@ -36,16 +37,16 @@ std::vector<exprt> instantiate_not_contains(
     const exprt &i1=pair.second;
     const minus_exprt val(i0, i1);
     const and_exprt universal_bound(
-      binary_relation_exprt(axiom.univ_lower_bound(), ID_le, val),
-      binary_relation_exprt(axiom.univ_upper_bound(), ID_gt, val));
+      binary_relation_exprt(axiom.univ_lower_bound, ID_le, val),
+      binary_relation_exprt(axiom.univ_upper_bound, ID_gt, val));
     const exprt f = index_exprt(witnesses.at(axiom), val);
     const equal_exprt relevancy(f, i1);
-    const and_exprt premise(relevancy, axiom.premise(), universal_bound);
+    const and_exprt premise(relevancy, axiom.premise, universal_bound);
 
     const notequal_exprt differ(s0[i0], s1[i1]);
     const and_exprt existential_bound(
-      binary_relation_exprt(axiom.exists_lower_bound(), ID_le, i1),
-      binary_relation_exprt(axiom.exists_upper_bound(), ID_gt, i1));
+      binary_relation_exprt(axiom.exists_lower_bound, ID_le, i1),
+      binary_relation_exprt(axiom.exists_upper_bound, ID_gt, i1));
     const and_exprt body(differ, existential_bound);
 
     const implies_exprt lemma(premise, body);
diff --git a/src/solvers/refinement/string_constraint_instantiation.h b/src/solvers/refinement/string_constraint_instantiation.h
index b473c74ae3d..c7c96375350 100644
--- a/src/solvers/refinement/string_constraint_instantiation.h
+++ b/src/solvers/refinement/string_constraint_instantiation.h
@@ -18,6 +18,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 std::vector<exprt> instantiate_not_contains(
   const string_not_contains_constraintt &axiom,
   const std::set<std::pair<exprt, exprt>> &index_pairs,
-  const std::map<string_not_contains_constraintt, symbol_exprt> &witnesses);
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
+    &witnesses);
 
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index b2f772df520..798b8830dd5 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -64,7 +64,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   const namespacet &ns,
   bool use_counter_example,
   const union_find_replacet &symbol_resolve,
-  const std::map<string_not_contains_constraintt, symbol_exprt>
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
     &not_contain_witnesses);
 
 static void initial_index_set(
@@ -113,7 +113,8 @@ static std::vector<exprt> instantiate(
   const string_not_contains_constraintt &axiom,
   const index_set_pairt &index_set,
   const string_constraint_generatort &generator,
-  const std::map<string_not_contains_constraintt, symbol_exprt> &witnesses);
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
+    &witnesses);
 
 static optionalt<exprt> get_array(
   const std::function<exprt(const exprt &)> &super_get,
@@ -231,7 +232,7 @@ static std::vector<exprt> generate_instantiations(
   const string_constraint_generatort &generator,
   const index_set_pairt &index_set,
   const string_axiomst &axioms,
-  const std::map<string_not_contains_constraintt, symbol_exprt>
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
     &not_contain_witnesses)
 {
   std::vector<exprt> lemmas;
@@ -716,16 +717,17 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     generator.constraints.not_contains.end(),
     std::back_inserter(axioms.not_contains),
     [&](string_not_contains_constraintt axiom) {
-      symbol_resolve.replace_expr(axiom);
+      replace(symbol_resolve, axiom);
       return axiom;
     });
 
   // Used to store information about witnesses for not_contains constraints
-  std::map<string_not_contains_constraintt, symbol_exprt> not_contain_witnesses;
+  std::unordered_map<string_not_contains_constraintt, symbol_exprt>
+    not_contain_witnesses;
   for(const auto &nc_axiom : axioms.not_contains)
   {
     const auto &witness_type = [&] {
-      const auto &rtype = to_array_type(nc_axiom.s0().type());
+      const auto &rtype = to_array_type(nc_axiom.s0.type());
       const typet &index_type = rtype.size().type();
       return array_typet(index_type, infinity_exprt(index_type));
     }();
@@ -1194,12 +1196,12 @@ static exprt negation_of_not_contains_constraint(
 {
   // If the for all is vacuously true, the negation is false.
   const auto lbe =
-    numeric_cast_v<mp_integer>(get(constraint.exists_lower_bound()));
+    numeric_cast_v<mp_integer>(get(constraint.exists_lower_bound));
   const auto ube =
-    numeric_cast_v<mp_integer>(get(constraint.exists_upper_bound()));
+    numeric_cast_v<mp_integer>(get(constraint.exists_upper_bound));
   const auto univ_bounds = and_exprt(
-    binary_relation_exprt(get(constraint.univ_lower_bound()), ID_le, univ_var),
-    binary_relation_exprt(get(constraint.univ_upper_bound()), ID_gt, univ_var));
+    binary_relation_exprt(get(constraint.univ_lower_bound), ID_le, univ_var),
+    binary_relation_exprt(get(constraint.univ_upper_bound), ID_gt, univ_var));
 
   // The negated existential becomes an universal, and this is the unrolling of
   // that universal quantifier.
@@ -1209,12 +1211,12 @@ static exprt negation_of_not_contains_constraint(
   {
     const constant_exprt i_expr = from_integer(i, univ_var.type());
     const exprt s0_char =
-      get(index_exprt(constraint.s0(), plus_exprt(univ_var, i_expr)));
-    const exprt s1_char = get(index_exprt(constraint.s1(), i_expr));
+      get(index_exprt(constraint.s0, plus_exprt(univ_var, i_expr)));
+    const exprt s1_char = get(index_exprt(constraint.s1, i_expr));
     conjuncts.push_back(equal_exprt(s0_char, s1_char));
   }
   const exprt equal_strings = conjunction(conjuncts);
-  return and_exprt(univ_bounds, get(constraint.premise()), equal_strings);
+  return and_exprt(univ_bounds, get(constraint.premise), equal_strings);
 }
 
 /// Debugging function which outputs the different steps an axiom goes through
@@ -1249,7 +1251,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   const namespacet &ns,
   bool use_counter_example,
   const union_find_replacet &symbol_resolve,
-  const std::map<string_not_contains_constraintt, symbol_exprt>
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
     &not_contain_witnesses)
 {
   const auto eom=messaget::eom;
@@ -1317,7 +1319,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   {
     const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i];
     const symbol_exprt univ_var = generator.fresh_symbol(
-      "not_contains_univ_var", nc_axiom.s0().length().type());
+      "not_contains_univ_var", nc_axiom.s0.length().type());
     const exprt negated_axiom = negation_of_not_contains_constraint(
       nc_axiom, univ_var, [&](const exprt &expr) {
         return simplify_expr(get(expr), ns); });
@@ -1742,8 +1744,8 @@ static void initial_index_set(
   const namespacet &ns,
   const string_not_contains_constraintt &axiom)
 {
-  auto it=axiom.premise().depth_begin();
-  const auto end=axiom.premise().depth_end();
+  auto it = axiom.premise.depth_begin();
+  const auto end = axiom.premise.depth_end();
   while(it!=end)
   {
     if(it->id() == ID_index && is_char_type(it->type()))
@@ -1761,9 +1763,8 @@ static void initial_index_set(
   }
 
   const minus_exprt kminus1(
-    axiom.exists_upper_bound(),
-    from_integer(1, axiom.exists_upper_bound().type()));
-  add_to_index_set(index_set, ns, axiom.s1().content(), kminus1);
+    axiom.exists_upper_bound, from_integer(1, axiom.exists_upper_bound.type()));
+  add_to_index_set(index_set, ns, axiom.s1.content(), kminus1);
 }
 
 /// Add to the index set all the indices that appear in the formula
@@ -1887,10 +1888,11 @@ static std::vector<exprt> instantiate(
   const string_not_contains_constraintt &axiom,
   const index_set_pairt &index_set,
   const string_constraint_generatort &generator,
-  const std::map<string_not_contains_constraintt, symbol_exprt> &witnesses)
+  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
+    &witnesses)
 {
-  const array_string_exprt &s0 = axiom.s0();
-  const array_string_exprt &s1 = axiom.s1();
+  const array_string_exprt &s0 = axiom.s0;
+  const array_string_exprt &s1 = axiom.s1;
 
   const auto &index_set0=index_set.cumulative.find(s0.content());
   const auto &index_set1=index_set.cumulative.find(s1.content());
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 595096bec87..4d2b2b4a43d 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -582,7 +582,6 @@ IREP_ID_ONE(push_catch)
 IREP_ID_ONE(pop_catch)
 IREP_ID_ONE(exception_landingpad)
 IREP_ID_ONE(length_upper_bound)
-IREP_ID_ONE(string_not_contains_constraint)
 IREP_ID_ONE(cprover_associate_array_to_pointer_func)
 IREP_ID_ONE(cprover_associate_length_to_array_func)
 IREP_ID_ONE(cprover_char_literal_func)