diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index d2c76eb6faa..74d341a24c9 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -48,7 +48,10 @@ class string_constraint_generatort final
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
-  const std::vector<exprt> &get_axioms() const;
+  const std::vector<exprt> &get_lemmas() const;
+  const std::vector<string_constraintt> &get_constraints() const;
+  const std::vector<string_not_contains_constraintt> &
+  get_not_contains_constraints() const;
 
   /// Boolean symbols for the results of some string functions
   const std::vector<symbol_exprt> &get_boolean_symbols() const;
@@ -349,7 +352,9 @@ class string_constraint_generatort final
   unsigned symbol_count=0;
   const messaget message;
 
-  std::vector<exprt> axioms;
+  std::vector<exprt> lemmas;
+  std::vector<string_constraintt> constraints;
+  std::vector<string_not_contains_constraintt> not_contains_constraints;
   std::vector<symbol_exprt> boolean_symbols;
   std::vector<symbol_exprt> index_symbols;
   const namespacet ns;
diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp
index a2e67a3ea82..1f61a769208 100644
--- a/src/solvers/refinement/string_constraint_generator_code_points.cpp
+++ b/src/solvers/refinement/string_constraint_generator_code_points.cpp
@@ -41,27 +41,27 @@ exprt string_constraint_generatort::add_axioms_for_code_point(
 
   binary_relation_exprt small(code_point, ID_lt, hex010000);
   implies_exprt a1(small, res.axiom_for_has_length(1));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   implies_exprt a2(not_exprt(small), res.axiom_for_has_length(2));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);
   implies_exprt a3(small, equal_exprt(res[0], code_point_as_char));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   plus_exprt first_char(
     hexD800, div_exprt(minus_exprt(code_point, hex010000), hex0400));
   implies_exprt a4(
     not_exprt(small),
     equal_exprt(res[0], typecast_exprt(first_char, char_type)));
-  axioms.push_back(a4);
+  lemmas.push_back(a4);
 
   plus_exprt second_char(hexDC00, mod_exprt(code_point, hex0400));
   implies_exprt a5(
     not_exprt(small),
     equal_exprt(res[1], typecast_exprt(second_char, char_type)));
-  axioms.push_back(a5);
+  lemmas.push_back(a5);
 
   return from_integer(0, get_return_code_type());
 }
@@ -136,8 +136,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
     is_low_surrogate(str[plus_exprt_with_overflow_check(pos, index1)]);
   const and_exprt return_pair(is_high_surrogate(str[pos]), is_low);
 
-  axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
-  axioms.push_back(
+  lemmas.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
+  lemmas.push_back(
     implies_exprt(not_exprt(return_pair), equal_exprt(result, char1_as_int)));
   return result;
 }
@@ -167,8 +167,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   const and_exprt return_pair(
     is_high_surrogate(char1), is_low_surrogate(char2));
 
-  axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
-  axioms.push_back(
+  lemmas.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
+  lemmas.push_back(
     implies_exprt(not_exprt(return_pair), equal_exprt(result, char2_as_int)));
   return result;
 }
@@ -189,8 +189,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const symbol_exprt result = fresh_symbol("code_point_count", return_type);
   const minus_exprt length(end, begin);
   const div_exprt minimum(length, from_integer(2, length.type()));
-  axioms.push_back(binary_relation_exprt(result, ID_le, length));
-  axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
+  lemmas.push_back(binary_relation_exprt(result, ID_le, length));
+  lemmas.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
   return result;
 }
@@ -212,8 +212,8 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
 
   const exprt minimum = plus_exprt_with_overflow_check(index, offset);
   const exprt maximum = plus_exprt_with_overflow_check(minimum, offset);
-  axioms.push_back(binary_relation_exprt(result, ID_le, maximum));
-  axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
+  lemmas.push_back(binary_relation_exprt(result, ID_le, maximum));
+  lemmas.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
   return result;
 }
diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp
index e59e8ef4ba7..7b8590e7836 100644
--- a/src/solvers/refinement/string_constraint_generator_comparison.cpp
+++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp
@@ -40,11 +40,11 @@ exprt string_constraint_generatort::add_axioms_for_equals(
 
 
   implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
   string_constraintt a2(qvar, s1.length(), eq, equal_exprt(s1[qvar], s2[qvar]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
   exprt zero=from_integer(0, index_type);
@@ -56,7 +56,7 @@ exprt string_constraint_generatort::add_axioms_for_equals(
     notequal_exprt(s1.length(), s2.length()),
     equal_exprt(witness, from_integer(-1, index_type)));
   implies_exprt a3(not_exprt(eq), or_exprt(diff_length, witnessing));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   return tc_eq;
 }
@@ -124,14 +124,14 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   const typet index_type = s1.length().type();
 
   const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   const symbol_exprt qvar =
     fresh_univ_index("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
   const string_constraintt a2(qvar, s1.length(), eq, constr2);
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   const symbol_exprt witness =
     fresh_exist_index("witness_unequal_ignore_case", index_type);
@@ -147,7 +147,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     or_exprt(
       notequal_exprt(s1.length(), s2.length()),
       and_exprt(bound_witness, witness_diff)));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   return typecast_exprt(eq, f.type());
 }
@@ -183,7 +183,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
         and_exprt(str.axiom_for_length_gt(i), axiom_for_is_positive_index(i))));
-    axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
+    lemmas.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
   return hash;
 }
@@ -220,12 +220,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const equal_exprt res_null(res, from_integer(0, return_type));
   const implies_exprt a1(res_null, equal_exprt(s1.length(), s2.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   const symbol_exprt i = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a2(
     i, s1.length(), res_null, equal_exprt(s1[i], s2[i]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
   const equal_exprt ret_char_diff(
@@ -251,12 +251,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
     and_exprt(
       binary_relation_exprt(x, ID_ge, from_integer(0, return_type)),
       or_exprt(cond1, cond2)));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   const symbol_exprt i2 = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a4(
     i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   return res;
 }
@@ -287,14 +287,14 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern(
   exprt::operandst disj;
   for(auto it : intern_of_string)
     disj.push_back(equal_exprt(intern, it.second));
-  axioms.push_back(disjunction(disj));
+  lemmas.push_back(disjunction(disj));
 
   // WARNING: the specification may be incomplete or incorrect
   for(auto it : intern_of_string)
     if(it.second!=str)
     {
       symbol_exprt i=fresh_exist_index("index_intern", index_type);
-      axioms.push_back(
+      lemmas.push_back(
         or_exprt(
           equal_exprt(it.second, intern),
           or_exprt(
diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp
index 1c002590ef2..fa38ac46bc1 100644
--- a/src/solvers/refinement/string_constraint_generator_concat.cpp
+++ b/src/solvers/refinement/string_constraint_generator_concat.cpp
@@ -49,20 +49,20 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   exprt res_length=plus_exprt_with_overflow_check(
     s1.length(), minus_exprt(end_index, start_index));
   implies_exprt a1(prem, equal_exprt(res.length(), res_length));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length()));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
   string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  axioms.push_back(a3);
+  constraints.push_back(a3);
 
   symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
   equal_exprt res_eq(
     res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]);
   string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq);
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   // We should have a enum type for the possible error codes
   return from_integer(0, res.length().type());
@@ -87,14 +87,14 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   const typet &index_type = res.length().type();
   const equal_exprt a1(
     res.length(), plus_exprt(s1.length(), from_integer(1, index_type)));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
   string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   equal_exprt a3(res[s1.length()], c);
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   // We should have a enum type for the possible error codes
   return from_integer(0, get_return_code_type());
diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp
index fad3a2d9e3d..0ed64b37a95 100644
--- a/src/solvers/refinement/string_constraint_generator_constants.cpp
+++ b/src/solvers/refinement/string_constraint_generator_constants.cpp
@@ -45,12 +45,12 @@ exprt string_constraint_generatort::add_axioms_for_constant(
     const exprt idx = from_integer(i, index_type);
     const exprt c = from_integer(str[i], char_type);
     const equal_exprt lemma(res[idx], c);
-    axioms.push_back(implies_exprt(guard, lemma));
+    lemmas.push_back(implies_exprt(guard, lemma));
   }
 
   const exprt s_length = from_integer(str.size(), index_type);
 
-  axioms.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
+  lemmas.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
   return from_integer(0, get_return_code_type());
 }
 
@@ -63,7 +63,7 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
 {
   PRECONDITION(f.arguments().size() == 2);
   exprt length = f.arguments()[0];
-  axioms.push_back(equal_exprt(length, from_integer(0, length.type())));
+  lemmas.push_back(equal_exprt(length, from_integer(0, length.type())));
   return from_integer(0, get_return_code_type());
 }
 
diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp
index cd1518b5dd9..7e084f872f8 100644
--- a/src/solvers/refinement/string_constraint_generator_float.cpp
+++ b/src/solvers/refinement/string_constraint_generator_float.cpp
@@ -251,7 +251,7 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
 
   and_exprt a1(res.axiom_for_length_gt(1),
                res.axiom_for_length_le(max));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
 
@@ -289,10 +289,10 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
   }
 
   exprt a2=conjunction(digit_constraints);
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   equal_exprt a3(int_expr, sum);
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   return from_integer(0, signedbv_typet(32));
 }
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 295c18df903..77086d849f3 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -47,17 +47,17 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   and_exprt a1(
     binary_relation_exprt(index, ID_ge, minus1),
     binary_relation_exprt(index, ID_lt, str.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   implies_exprt a3(
     contains,
     and_exprt(
       binary_relation_exprt(from_index, ID_le, index),
       equal_exprt(str[index], c)));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   const auto zero = from_integer(0, index_type);
   const if_exprt lower_bound(
@@ -66,7 +66,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a4(
     n, lower_bound, index, contains, not_exprt(equal_exprt(str[n], c)));
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a5(
@@ -75,7 +75,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
     str.length(),
     not_exprt(contains),
     not_exprt(equal_exprt(str[m], c)));
-  axioms.push_back(a5);
+  constraints.push_back(a5);
 
   return index;
 }
@@ -119,12 +119,12 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
       binary_relation_exprt(from_index, ID_le, offset),
       binary_relation_exprt(
         offset, ID_le, minus_exprt(haystack.length(), needle.length()))));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   equal_exprt a2(
     not_exprt(contains),
     equal_exprt(offset, from_integer(-1, index_type)));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   string_constraintt a3(
@@ -132,7 +132,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     needle.length(),
     contains,
     equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
-  axioms.push_back(a3);
+  constraints.push_back(a3);
 
   // 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]
@@ -144,7 +144,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     needle.length(),
     haystack,
     needle);
-  axioms.push_back(a4);
+  not_contains_constraints.push_back(a4);
 
   string_not_contains_constraintt a5(
     from_index,
@@ -156,12 +156,12 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     needle.length(),
     haystack,
     needle);
-  axioms.push_back(a5);
+  not_contains_constraints.push_back(a5);
 
   const implies_exprt a6(
     equal_exprt(needle.length(), from_integer(0, index_type)),
     equal_exprt(offset, from_index));
-  axioms.push_back(a6);
+  lemmas.push_back(a6);
 
   return offset;
 }
@@ -212,17 +212,17 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
       binary_relation_exprt(
         offset, ID_le, minus_exprt(haystack.length(), needle.length())),
       binary_relation_exprt(offset, ID_le, from_index)));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   equal_exprt a2(
     not_exprt(contains),
     equal_exprt(offset, from_integer(-1, index_type)));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
   string_constraintt a3(qvar, needle.length(), contains, constr3);
-  axioms.push_back(a3);
+  constraints.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
   minus_exprt length_diff(haystack.length(), needle.length());
@@ -239,7 +239,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     needle.length(),
     haystack,
     needle);
-  axioms.push_back(a4);
+  not_contains_constraints.push_back(a4);
 
   string_not_contains_constraintt a5(
     from_integer(0, index_type),
@@ -249,12 +249,12 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     needle.length(),
     haystack,
     needle);
-  axioms.push_back(a5);
+  not_contains_constraints.push_back(a5);
 
   const implies_exprt a6(
     equal_exprt(needle.length(), from_integer(0, index_type)),
     equal_exprt(offset, from_index));
-  axioms.push_back(a6);
+  lemmas.push_back(a6);
 
   return offset;
 }
@@ -343,13 +343,13 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
     binary_relation_exprt(index, ID_ge, minus1),
     binary_relation_exprt(index, ID_le, from_index),
     binary_relation_exprt(index, ID_lt, str.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   const notequal_exprt a2(contains, equal_exprt(index, minus1));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   const implies_exprt a3(contains, equal_exprt(str[index], c));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   const exprt index1 = from_integer(1, index_type);
   const exprt from_index_plus_one =
@@ -366,12 +366,12 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
     end_index,
     contains,
     notequal_exprt(str[n], c));
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
   const string_constraintt a5(
     m, end_index, not_exprt(contains), notequal_exprt(str[m], c));
-  axioms.push_back(a5);
+  constraints.push_back(a5);
 
   return index;
 }
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index c73e450fdbd..77d6d600a68 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -35,9 +35,21 @@ string_constraint_generatort::string_constraint_generatort(
 {
 }
 
-const std::vector<exprt> &string_constraint_generatort::get_axioms() const
+const std::vector<exprt> &string_constraint_generatort::get_lemmas() const
 {
-  return axioms;
+  return lemmas;
+}
+
+const std::vector<string_constraintt> &
+string_constraint_generatort::get_constraints() const
+{
+  return constraints;
+}
+
+const std::vector<string_not_contains_constraintt> &
+string_constraint_generatort::get_not_contains_constraints() const
+{
+  return not_contains_constraints;
 }
 
 const std::vector<symbol_exprt> &
@@ -136,7 +148,7 @@ plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check(
   implies_exprt no_overflow(equal_exprt(neg1, neg2),
                             equal_exprt(neg1, neg_sum));
 
-  axioms.push_back(no_overflow);
+  lemmas.push_back(no_overflow);
 
   return sum;
 }
@@ -291,7 +303,7 @@ exprt string_constraint_generatort::associate_length_to_array(
   const exprt &new_length = f.arguments()[1];
 
   const auto &length = get_length_of_string_array(array_expr);
-  axioms.push_back(equal_exprt(length, new_length));
+  lemmas.push_back(equal_exprt(length, new_length));
   return from_integer(0, f.type());
 }
 
@@ -322,10 +334,10 @@ void string_constraint_generatort::add_default_axioms(
     return;
 
   const exprt index_zero = from_integer(0, s.length().type());
-  axioms.push_back(s.axiom_for_length_ge(index_zero));
+  lemmas.push_back(s.axiom_for_length_ge(index_zero));
 
   if(max_string_length!=std::numeric_limits<size_t>::max())
-    axioms.push_back(s.axiom_for_length_le(max_string_length));
+    lemmas.push_back(s.axiom_for_length_le(max_string_length));
 }
 
 /// Add constraint on characters of a string.
@@ -359,7 +371,7 @@ void string_constraint_generatort::add_constraint_on_characters(
     binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
     binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
   const string_constraintt sc(qvar, start, end, true_exprt(), char_in_set);
-  axioms.push_back(sc);
+  constraints.push_back(sc);
 }
 
 /// Add axioms to ensure all characters of a string belong to a given set.
@@ -620,6 +632,6 @@ exprt string_constraint_generatort::add_axioms_for_char_at(
   PRECONDITION(f.arguments().size() == 2);
   array_string_exprt str = get_string_expr(f.arguments()[0]);
   symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
-  axioms.push_back(equal_exprt(char_sym, str[f.arguments()[1]]));
+  lemmas.push_back(equal_exprt(char_sym, str[f.arguments()[1]]));
   return char_sym;
 }
diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp
index 3186451e32e..6a2c7d0d8a3 100644
--- a/src/solvers/refinement/string_constraint_generator_testing.cpp
+++ b/src/solvers/refinement/string_constraint_generator_testing.cpp
@@ -40,7 +40,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
     isprefix,
     str.axiom_for_length_ge(plus_exprt_with_overflow_check(
       prefix.length(), offset)));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type);
   string_constraintt a2(
@@ -48,7 +48,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
     prefix.length(),
     isprefix,
     equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type);
   and_exprt witness_diff(
@@ -61,7 +61,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
     witness_diff);
 
   implies_exprt a3(not_exprt(isprefix), s0_notpref_s1);
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
   return isprefix;
 }
 
@@ -109,8 +109,8 @@ exprt string_constraint_generatort::add_axioms_for_is_empty(
 
   symbol_exprt is_empty=fresh_boolean("is_empty");
   array_string_exprt s0 = get_string_expr(f.arguments()[0]);
-  axioms.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0)));
-  axioms.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty));
+  lemmas.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0)));
+  lemmas.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty));
   return typecast_exprt(is_empty, f.type());
 }
 
@@ -148,14 +148,14 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   const typet &index_type=s0.length().type();
 
   implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
   exprt qvar_shifted=plus_exprt(
     qvar, minus_exprt(s1.length(), s0.length()));
   string_constraintt a2(
     qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
   exprt shifted=plus_exprt(
@@ -171,7 +171,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
         axiom_for_is_positive_index(witness))));
   implies_exprt a3(not_exprt(issuffix), constr3);
 
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
   return tc_issuffix;
 }
 
@@ -206,25 +206,25 @@ exprt string_constraint_generatort::add_axioms_for_contains(
     fresh_exist_index("startpos_contains", index_type);
 
   const implies_exprt a1(contains, s0.axiom_for_length_ge(s1.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   minus_exprt length_diff(s0.length(), s1.length());
   and_exprt bounds(
     axiom_for_is_positive_index(startpos),
     binary_relation_exprt(startpos, ID_le, length_diff));
   implies_exprt a2(contains, bounds);
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   implies_exprt a3(
     not_exprt(contains),
     equal_exprt(startpos, from_integer(-1, index_type)));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
   exprt qvar_shifted=plus_exprt(qvar, startpos);
   string_constraintt a4(
     qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   string_not_contains_constraintt a5(
     from_integer(0, index_type),
@@ -234,7 +234,7 @@ exprt string_constraint_generatort::add_axioms_for_contains(
     s1.length(),
     s0,
     s1);
-  axioms.push_back(a5);
+  not_contains_constraints.push_back(a5);
 
   return typecast_exprt(contains, f.type());
 }
diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index c865699b4dd..e589ff5c65d 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -48,7 +48,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
   // a2 : forall i<|res|. i < |s1|  ==> res[i] = s1[i]
   // a3 : forall i<|res|. i >= |s1| ==> res[i] = 0
 
-  axioms.push_back(res.axiom_for_has_length(k));
+  lemmas.push_back(res.axiom_for_has_length(k));
 
   symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
   string_constraintt a2(
@@ -56,7 +56,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
     res.length(),
     s1.axiom_for_length_gt(idx),
     equal_exprt(s1[idx], res[idx]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type);
   string_constraintt a3(
@@ -64,7 +64,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
     res.length(),
     s1.axiom_for_length_le(idx2),
     equal_exprt(res[idx2], constant_char(0, char_type)));
-  axioms.push_back(a3);
+  constraints.push_back(a3);
 
   return from_integer(0, signedbv_typet(32));
 }
@@ -131,21 +131,21 @@ exprt string_constraint_generatort::add_axioms_for_substring(
   implies_exprt a1(
     binary_relation_exprt(start, ID_lt, end),
     res.axiom_for_has_length(minus_exprt(end, start)));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   exprt is_empty=res.axiom_for_has_length(from_integer(0, index_type));
   implies_exprt a2(binary_relation_exprt(start, ID_ge, end), is_empty);
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   // Warning: check what to do if the string is not long enough
-  axioms.push_back(str.axiom_for_length_ge(end));
+  lemmas.push_back(str.axiom_for_length_ge(end));
 
   symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type);
   string_constraintt a4(idx,
                         res.length(),
                         equal_exprt(res[idx],
                         str[plus_exprt(start, idx)]));
-  axioms.push_back(a4);
+  constraints.push_back(a4);
   return from_integer(0, signedbv_typet(32));
 }
 
@@ -189,25 +189,25 @@ exprt string_constraint_generatort::add_axioms_for_trim(
 
   exprt a1=str.axiom_for_length_ge(
     plus_exprt_with_overflow_check(idx, res.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   exprt a3=str.axiom_for_length_ge(idx);
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   exprt a4=res.axiom_for_length_ge(
     from_integer(0, index_type));
-  axioms.push_back(a4);
+  lemmas.push_back(a4);
 
   exprt a5 = res.axiom_for_length_le(str.length());
-  axioms.push_back(a5);
+  lemmas.push_back(a5);
 
   symbol_exprt n=fresh_univ_index("QA_index_trim", index_type);
   binary_relation_exprt non_print(str[n], ID_le, space_char);
   string_constraintt a6(n, idx, non_print);
-  axioms.push_back(a6);
+  constraints.push_back(a6);
 
   symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type);
   minus_exprt bound(str.length(), plus_exprt_with_overflow_check(idx,
@@ -218,12 +218,12 @@ exprt string_constraint_generatort::add_axioms_for_trim(
     space_char);
 
   string_constraintt a7(n2, bound, eqn2);
-  axioms.push_back(a7);
+  constraints.push_back(a7);
 
   symbol_exprt n3=fresh_univ_index("QA_index_trim3", index_type);
   equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
   string_constraintt a8(n3, res.length(), eqn3);
-  axioms.push_back(a8);
+  constraints.push_back(a8);
 
   minus_exprt index_before(
     plus_exprt_with_overflow_check(idx, res.length()),
@@ -234,7 +234,7 @@ exprt string_constraint_generatort::add_axioms_for_trim(
     and_exprt(
       binary_relation_exprt(str[idx], ID_gt, space_char),
       no_space_before));
-  axioms.push_back(a9);
+  lemmas.push_back(a9);
   return from_integer(0, f.type());
 }
 
@@ -273,7 +273,7 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case(
   // information from the UnicodeData file.
 
   equal_exprt a1(res.length(), str.length());
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt idx=fresh_univ_index("QA_lower_case", index_type);
   exprt::operandst upper_case;
@@ -306,7 +306,7 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case(
   if_exprt conditional_convert(is_upper_case, converted, non_converted);
 
   string_constraintt a2(idx, res.length(), conditional_convert);
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   return from_integer(0, f.type());
 }
@@ -343,7 +343,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   // from the UnicodeData file.
 
   equal_exprt a1(res.length(), str.length());
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type);
   exprt is_lower_case=and_exprt(
@@ -353,7 +353,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff));
   implies_exprt body1(is_lower_case, convert);
   string_constraintt a2(idx1, res.length(), body1);
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type);
   exprt is_not_lower_case=not_exprt(and_exprt(
@@ -362,7 +362,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   equal_exprt eq(res[idx2], str[idx2]);
   implies_exprt body2(is_not_lower_case, eq);
   string_constraintt a3(idx2, res.length(), body2);
-  axioms.push_back(a3);
+  constraints.push_back(a3);
   return from_integer(0, signedbv_typet(32));
 }
 
@@ -412,13 +412,14 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
   const exprt &character = f.arguments()[4];
 
   const binary_relation_exprt out_of_bounds(position, ID_ge, str.length());
-  axioms.push_back(equal_exprt(res.length(), str.length()));
-  axioms.push_back(equal_exprt(res[position], character));
+  lemmas.push_back(equal_exprt(res.length(), str.length()));
+  lemmas.push_back(equal_exprt(res[position], character));
   const symbol_exprt q = fresh_univ_index("QA_char_set", position.type());
   equal_exprt a3_body(res[q], str[q]);
   notequal_exprt a3_guard(q, position);
-  axioms.push_back(string_constraintt(
-    q, from_integer(0, q.type()), res.length(), a3_guard, a3_body));
+  constraints.push_back(
+    string_constraintt(
+      q, from_integer(0, q.type()), res.length(), a3_guard, a3_body));
   return if_exprt(
     out_of_bounds, from_integer(1, f.type()), from_integer(0, f.type()));
 }
@@ -484,7 +485,7 @@ exprt string_constraint_generatort::add_axioms_for_replace(
     const auto old_char=maybe_chars->first;
     const auto new_char=maybe_chars->second;
 
-    axioms.push_back(equal_exprt(res.length(), str.length()));
+    lemmas.push_back(equal_exprt(res.length(), str.length()));
 
     symbol_exprt qvar = fresh_univ_index("QA_replace", str.length().type());
     implies_exprt case1(
@@ -494,7 +495,7 @@ exprt string_constraint_generatort::add_axioms_for_replace(
       not_exprt(equal_exprt(str[qvar], old_char)),
       equal_exprt(res[qvar], str[qvar]));
     string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
-    axioms.push_back(a2);
+    constraints.push_back(a2);
     return from_integer(0, f.type());
   }
   return from_integer(1, f.type());
diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp
index 45c8799fca1..920f0de801a 100644
--- a/src/solvers/refinement/string_constraint_generator_valueof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp
@@ -89,24 +89,24 @@ exprt string_constraint_generatort::add_axioms_from_bool(
 
   std::string str_true="true";
   implies_exprt a1(eq, res.axiom_for_has_length(str_true.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   for(std::size_t i=0; i<str_true.length(); i++)
   {
     exprt chr=from_integer(str_true[i], char_type);
     implies_exprt a2(eq, equal_exprt(res[i], chr));
-    axioms.push_back(a2);
+    lemmas.push_back(a2);
   }
 
   std::string str_false="false";
   implies_exprt a3(not_exprt(eq), res.axiom_for_has_length(str_false.length()));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   for(std::size_t i=0; i<str_false.length(); i++)
   {
     exprt chr=from_integer(str_false[i], char_type);
     implies_exprt a4(not_exprt(eq), equal_exprt(res[i], chr));
-    axioms.push_back(a4);
+    lemmas.push_back(a4);
   }
 
   return from_integer(0, signedbv_typet(32));
@@ -216,9 +216,8 @@ exprt string_constraint_generatort::add_axioms_from_int_hex(
   exprt f_char=constant_char('f', char_type);
 
   size_t max_size=8;
-  axioms.push_back(
-    and_exprt(res.axiom_for_length_gt(0),
-              res.axiom_for_length_le(max_size)));
+  lemmas.push_back(
+    and_exprt(res.axiom_for_length_gt(0), res.axiom_for_length_le(max_size)));
 
   for(size_t size=1; size<=max_size; size++)
   {
@@ -242,12 +241,12 @@ exprt string_constraint_generatort::add_axioms_from_int_hex(
     }
 
     equal_exprt premise(res.axiom_for_has_length(size));
-    axioms.push_back(
+    lemmas.push_back(
       implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
 
     // disallow 0s at the beginning
     if(size>1)
-      axioms.push_back(
+      lemmas.push_back(
         implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
   }
   return from_integer(0, get_return_code_type());
@@ -296,7 +295,7 @@ exprt string_constraint_generatort::add_axioms_from_char(
   const exprt &c)
 {
   and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1));
-  axioms.push_back(lemma);
+  lemmas.push_back(lemma);
   return from_integer(0, get_return_code_type());
 }
 
@@ -330,30 +329,30 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
 
   // |str| > 0
   const exprt non_empty=str.axiom_for_length_ge(from_integer(1, index_type));
-  axioms.push_back(non_empty);
+  lemmas.push_back(non_empty);
 
   if(strict_formatting)
   {
     // str[0] = '-' || is_digit_with_radix(str[0], radix)
     const or_exprt correct_first(starts_with_minus, starts_with_digit);
-    axioms.push_back(correct_first);
+    lemmas.push_back(correct_first);
   }
   else
   {
     // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix)
     const or_exprt correct_first(
       starts_with_minus, starts_with_digit, starts_with_plus);
-    axioms.push_back(correct_first);
+    lemmas.push_back(correct_first);
   }
 
   // str[0]='+' or '-' ==> |str| > 1
   const implies_exprt contains_digit(
     or_exprt(starts_with_minus, starts_with_plus),
     str.axiom_for_length_ge(from_integer(2, index_type)));
-  axioms.push_back(contains_digit);
+  lemmas.push_back(contains_digit);
 
   // |str| <= max_size
-  axioms.push_back(str.axiom_for_length_le(max_size));
+  lemmas.push_back(str.axiom_for_length_le(max_size));
 
   // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
   // We unfold the above because we know that it will be used for all i up to
@@ -365,7 +364,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
       str.axiom_for_length_ge(from_integer(index+1, index_type)),
       is_digit_with_radix(
         str[index], strict_formatting, radix_as_char, radix_ul));
-    axioms.push_back(character_at_index_is_digit);
+    lemmas.push_back(character_at_index_is_digit);
   }
 
   if(strict_formatting)
@@ -376,12 +375,12 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
     const implies_exprt no_leading_zero(
       equal_exprt(chr, zero_char),
       str.axiom_for_has_length(from_integer(1, index_type)));
-    axioms.push_back(no_leading_zero);
+    lemmas.push_back(no_leading_zero);
 
     // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
     implies_exprt no_leading_zero_after_minus(
       starts_with_minus, not_exprt(equal_exprt(str[1], zero_char)));
-    axioms.push_back(no_leading_zero_after_minus);
+    lemmas.push_back(no_leading_zero_after_minus);
   }
 }
 
@@ -418,7 +417,7 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string(
   /// Deal with size==1 case separately. There are axioms from
   /// add_axioms_for_correct_number_format which say that the string must
   /// contain at least one digit, so we don't have to worry about "+" or "-".
-  axioms.push_back(
+  lemmas.push_back(
     implies_exprt(str.axiom_for_has_length(1), equal_exprt(input_int, sum)));
 
   for(size_t size=2; size<=max_string_length; size++)
@@ -462,18 +461,18 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string(
     if(!digit_constraints.empty())
     {
       const implies_exprt a5(premise, conjunction(digit_constraints));
-      axioms.push_back(a5);
+      lemmas.push_back(a5);
     }
 
     const implies_exprt a6(
       and_exprt(premise, not_exprt(starts_with_minus)),
       equal_exprt(input_int, sum));
-    axioms.push_back(a6);
+    lemmas.push_back(a6);
 
     const implies_exprt a7(
       and_exprt(premise, starts_with_minus),
       equal_exprt(input_int, unary_minus_exprt(sum)));
-    axioms.push_back(a7);
+    lemmas.push_back(a7);
   }
 }
 
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 3e3ed3a9479..712e80acad9 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -811,37 +811,50 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     supert::set_to(eq, true);
   }
 
-  const auto get = [this](const exprt &expr) { return this->get(expr); };
-  for(exprt axiom : generator.get_axioms())
-  {
-    symbol_resolve.replace_expr(axiom);
-    if(axiom.id()==ID_string_constraint)
-    {
-      string_constraintt univ_axiom = to_string_constraint(axiom);
+  const auto constraints = generator.get_constraints();
+  std::transform(
+    constraints.begin(),
+    constraints.end(),
+    std::back_inserter(axioms.universal),
+    [&](string_constraintt constraint) { // NOLINT
+      symbol_resolve.replace_expr(constraint);
       DATA_INVARIANT(
-        is_valid_string_constraint(error(), ns, univ_axiom),
+        is_valid_string_constraint(error(), ns, constraint),
         string_refinement_invariantt(
           "string constraints satisfy their invariant"));
-      axioms.universal.push_back(univ_axiom);
-    }
-    else if(axiom.id()==ID_string_not_contains_constraint)
-    {
-      string_not_contains_constraintt nc_axiom=
-        to_string_not_contains_constraint(axiom);
-      array_typet rtype = to_array_type(nc_axiom.s0().type());
+      return constraint;
+    });
+
+  const auto not_contains_constraints =
+    generator.get_not_contains_constraints();
+  std::transform(
+    not_contains_constraints.begin(),
+    not_contains_constraints.end(),
+    std::back_inserter(axioms.not_contains),
+    [&](string_not_contains_constraintt axiom) { // NOLINT
+      symbol_resolve.replace_expr(axiom);
+      return axiom;
+    });
+
+  for(const auto &nc_axiom : axioms.not_contains)
+  {
+    const auto &witness_type = [&] { // NOLINT
+      const auto &rtype = to_array_type(nc_axiom.s0().type());
       const typet &index_type = rtype.size().type();
-      array_typet witness_type(index_type, infinity_exprt(index_type));
-      generator.witness[nc_axiom]=
-        generator.fresh_symbol("not_contains_witness", witness_type);
-      axioms.not_contains.push_back(nc_axiom);
-    }
-    else
-    {
-      add_lemma(axiom);
-    }
+      return array_typet(index_type, infinity_exprt(index_type));
+    }();
+    generator.witness[nc_axiom] =
+      generator.fresh_symbol("not_contains_witness", witness_type);
+  }
+
+  for(exprt lemma : generator.get_lemmas())
+  {
+    symbol_resolve.replace_expr(lemma);
+    add_lemma(lemma);
   }
 
   // Initial try without index set
+  const auto get = [this](const exprt &expr) { return this->get(expr); };
   const decision_proceduret::resultt res=supert::dec_solve();
   if(res==resultt::D_SATISFIABLE)
   {
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index cab3aff3328..17149166e2a 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -94,12 +94,8 @@ class string_refinementt final: public bv_refinementt
   union_find_replacet symbol_resolve;
 
   std::vector<equal_exprt> equations;
-  std::list<std::pair<exprt, bool>> non_string_axioms;
 
-  // Map pointers to array symbols
-  std::map<exprt, symbol_exprt> pointer_map;
-
-  void add_lemma(const exprt &lemma, const bool _simplify = true);
+  void add_lemma(const exprt &lemma, bool simplify_lemma = true);
 };
 
 exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
index fe4d6d6bbe0..a5aa7eb4028 100644
--- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -8,12 +8,12 @@
 
 #include <testing-utils/catch.hpp>
 
-#include <solvers/refinement/string_constraint_instantiation.h>
-
-#include <solvers/sat/satcheck.h>
+#include <numeric>
+#include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
 #include <langapi/mode.h>
-#include <java_bytecode/java_bytecode_language.h>
+#include <solvers/refinement/string_constraint_instantiation.h>
+#include <solvers/sat/satcheck.h>
 #include <util/simplify_expr.h>
 #include <util/config.h>
 
@@ -193,28 +193,40 @@ SCENARIO("instantiate_not_contains",
     exprt res=generator.add_axioms_for_function_application(func);
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
-    for(exprt axiom : generator.get_axioms())
-    {
-      simplify(axiom, ns);
-      if(axiom.id()==ID_string_constraint)
-      {
-        string_constraintt sc=to_string_constraint(axiom);
-        axioms+=from_expr(ns, "", sc);
-      }
-      else if(axiom.id()==ID_string_not_contains_constraint)
-      {
-        string_not_contains_constraintt sc=
-          to_string_not_contains_constraint(axiom);
-        axioms+=from_expr(ns, "", sc);
-        generator.witness[sc]=
-          generator.fresh_symbol("w", t.witness_type());
+
+    const auto constraints = generator.get_constraints();
+    std::accumulate(
+      constraints.begin(),
+      constraints.end(),
+      axioms,
+      [&](const std::string &accu, string_constraintt sc) { // NOLINT
+        simplify(sc, ns);
+        return accu + from_expr(ns, "", sc) + "\n\n";
+      });
+
+    const auto nc_contraints = generator.get_not_contains_constraints();
+    axioms = std::accumulate(
+      nc_contraints.begin(),
+      nc_contraints.end(),
+      axioms,
+      [&](
+        const std::string &accu, string_not_contains_constraintt sc) { // NOLINT
+        simplify(sc, ns);
+        generator.witness[sc] = generator.fresh_symbol("w", t.witness_type());
         nc_axioms.push_back(sc);
-      }
-      else
-        axioms+=from_expr(ns, "", axiom);
+        return accu + from_expr(ns, "", sc) + "\n\n";
+      });
+
+    const auto lemmas = generator.get_lemmas();
+    axioms = std::accumulate(
+      lemmas.begin(),
+      lemmas.end(),
+      axioms,
+      [&](const std::string &accu, exprt axiom) { // NOLINT
+        simplify(axiom, ns);
+        return accu + from_expr(ns, "", axiom) + "\n\n";
+      });
 
-      axioms+="\n\n";
-    }
     INFO("Original axioms:\n");
     INFO(axioms);