diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 293d0419361..4a60c9b0577 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -180,6 +180,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
       refinement/string_refinement.cpp \
+      refinement/string_constraint.cpp \
       refinement/string_refinement_util.cpp \
       refinement/string_constraint_generator_code_points.cpp \
       refinement/string_constraint_generator_comparison.cpp \
diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp
new file mode 100644
index 00000000000..2e404dd209e
--- /dev/null
+++ b/src/solvers/refinement/string_constraint.cpp
@@ -0,0 +1,203 @@
+// Author: DiffBlue Ltd.
+
+#include <stack>
+#include "string_constraint.h"
+#include <util/simplify_expr.h>
+#include <util/expr_iterator.h>
+
+exprt string_constraintt::get_lower_bound() const
+{
+  return lower_bound ? *lower_bound : from_integer(0, upper_bound.type());
+}
+
+void replace(string_constraintt &axiom, const replace_mapt &symbol_resolve)
+{
+  replace_expr(symbol_resolve, axiom.index_guard);
+  replace_expr(symbol_resolve, axiom.body);
+  replace_expr(symbol_resolve, axiom.univ_var);
+  replace_expr(symbol_resolve, axiom.upper_bound);
+  if(axiom.lower_bound)
+    replace_expr(symbol_resolve, *axiom.lower_bound);
+}
+
+exprt univ_within_bounds(const string_constraintt &axiom)
+{
+  return and_exprt(
+    binary_relation_exprt(axiom.get_lower_bound(), ID_le, axiom.univ_var),
+    binary_relation_exprt(axiom.upper_bound, ID_gt, axiom.univ_var));
+}
+
+std::string to_string(const string_constraintt &expr)
+{
+  std::ostringstream out;
+  out << "forall " << format(expr.univ_var) << " in ["
+      << format(expr.get_lower_bound()) << ", " << format(expr.upper_bound)
+      << "). " << format(expr.index_guard) << " => " << format(expr.body);
+  return out.str();
+}
+
+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();
+}
+
+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);
+}
+
+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);
+}
+
+typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
+
+static array_index_mapt gather_indices(const exprt &expr)
+{
+  array_index_mapt indices;
+  std::for_each(
+    expr.depth_begin(),
+    expr.depth_end(),
+    [&](const exprt &expr) { // NOLINT
+      if(const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr))
+        indices[index_expr->array()].push_back(index_expr->index());
+    });
+  return indices;
+}
+
+/// \param expr: an expression
+/// \param var: a symbol
+/// \return Boolean telling whether `expr` is a linear function of `var`.
+/// \todo Add unit tests
+/// \related string_constraintt
+static bool
+is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
+{
+  for(auto it = expr.depth_begin(); it != expr.depth_end();)
+  {
+    if(
+      it->id() != ID_plus && it->id() != ID_minus &&
+      it->id() != ID_unary_minus && *it != var)
+    {
+      const auto find_qvar = std::find(it->depth_begin(), it->depth_end(), var);
+      if(find_qvar != it->depth_end())
+        return false;
+      else
+        it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+  return true;
+}
+
+/// The universally quantified variable is only allowed to occur in index
+/// expressions in the body of a string constraint. This function returns true
+/// if this is the case and false otherwise.
+/// \param [in] expr: The string constraint to check
+/// \return true if the universal variable only occurs in index expressions,
+///   false otherwise.
+static bool universal_only_in_index(const string_constraintt &expr)
+{
+  for(auto it = expr.body.depth_begin(); it != expr.body.depth_end();)
+  {
+    if(*it == expr.univ_var)
+      return false;
+    if(it->id() == ID_index)
+      it.next_sibling_or_parent();
+    else
+      ++it;
+  }
+  return true;
+}
+
+/// Checks the data invariant for \link string_constraintt \endlink
+/// \related string_constraintt
+/// \param stream: message stream
+/// \param ns: namespace
+/// \param [in] constraint: the string constraint to check
+/// \return whether the constraint satisfies the invariant
+bool is_valid_string_constraint(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const string_constraintt &constraint)
+{
+  const auto eom = messaget::eom;
+  // Condition 1: The index guard cannot contain any string indices
+  const array_index_mapt premise_indices =
+    gather_indices(constraint.index_guard);
+  if(!premise_indices.empty())
+  {
+    stream << "Index guard has indices: " << to_string(constraint)
+           << ", map: {";
+    for(const auto &pair : premise_indices)
+    {
+      stream << format(pair.first) << ": {";
+      for(const auto &i : pair.second)
+        stream << format(i) << ", ";
+    }
+    stream << "}}" << eom;
+    return false;
+  }
+
+  const array_index_mapt body_indices = gather_indices(constraint.body);
+  // Must validate for each string. Note that we have an invariant that the
+  // second value in the pair is non-empty.
+  for(const auto &pair : body_indices)
+  {
+    // Condition 2: All indices of the same string must be the of the same form
+    const exprt rep = pair.second.back();
+    for(size_t j = 0; j < pair.second.size() - 1; j++)
+    {
+      const exprt i = pair.second[j];
+      const equal_exprt equals(rep, i);
+      const exprt result = simplify_expr(equals, ns);
+      if(result.is_false())
+      {
+        stream << "Indices not equal: " << to_string(constraint)
+               << ", str: " << format(pair.first) << eom;
+        return false;
+      }
+    }
+
+    // Condition 3: f must be linear
+    if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
+    {
+      stream << "f is not linear: " << to_string(constraint)
+             << ", str: " << format(pair.first) << eom;
+      return false;
+    }
+
+    // Condition 4: the quantified variable can only occur in indices in the
+    // body
+    if(!universal_only_in_index(constraint))
+    {
+      stream << "Universal variable outside of index:" << to_string(constraint)
+             << eom;
+      return false;
+    }
+  }
+
+  return true;
+}
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index e72ead2495d..d372ed68a62 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -27,6 +27,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/format_type.h>
 #include <util/refined_string_type.h>
 #include <util/string_expr.h>
+#include <langapi/language_util.h>
+#include <util/union_find_replace.h>
 
 ///  ### Universally quantified string constraint
 ///
@@ -54,100 +56,53 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 ///      \f$f\f$ [explicitly stated, implied].
 ///
 /// \todo The fact that we follow this grammar is not enforced at the moment.
-class string_constraintt : public exprt
+class string_constraintt final
 {
 public:
-  // String constraints are of the form
-  // forall univ_var in [lower_bound,upper_bound[. premise => body
-
-  const exprt &premise() const
-  {
-    return op0();
-  }
-
-  const exprt &body() const
-  {
-    return op1();
-  }
-
-  const symbol_exprt &univ_var() const
-  {
-    return to_symbol_expr(op2());
-  }
-
-  const exprt &upper_bound() const
-  {
-    return op3();
-  }
-
-  const exprt &lower_bound() const
-  {
-    return operands()[4];
-  }
-
- private:
-  string_constraintt();
-
- public:
-  string_constraintt(
-    const symbol_exprt &_univ_var,
-    const exprt &bound_inf,
-    const exprt &bound_sup,
-    const exprt &body):
-    exprt(ID_string_constraint)
-  {
-    copy_to_operands(true_exprt(), body);
-    copy_to_operands(_univ_var, bound_sup, bound_inf);
-  }
-
-  // Default bound inferior is 0
-  string_constraintt(
-    const symbol_exprt &_univ_var,
-    const exprt &bound_sup,
-    const exprt &body):
-    string_constraintt(
-      _univ_var,
-      from_integer(0, _univ_var.type()),
-      bound_sup,
-      body)
-  {}
-
-  exprt univ_within_bounds() const
-  {
-    return and_exprt(
-      binary_relation_exprt(lower_bound(), ID_le, univ_var()),
-      binary_relation_exprt(upper_bound(), ID_gt, univ_var()));
-  }
+  /// String constraints are of the form
+  /// forall univ_var in [lower_bound,upper_bound[. index_guard => body
+  exprt index_guard = true_exprt(); // Index guard
+  exprt body;                       // value constraint
+  symbol_exprt univ_var;
+  exprt upper_bound;
+  optionalt<exprt> lower_bound; // empty defaults to 0
+
+  /// \return lower_bound if it has been set, expression for 0 otherwise
+  exprt get_lower_bound() const;
 };
 
-extern inline const string_constraintt &to_string_constraint(const exprt &expr)
+inline void
+replace(string_constraintt &axiom, const union_find_replacet &symbol_resolve)
 {
-  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
-  return static_cast<const string_constraintt &>(expr);
+  symbol_resolve.replace_expr(axiom.index_guard);
+  symbol_resolve.replace_expr(axiom.body);
+  symbol_resolve.replace_expr(axiom.univ_var);
+  symbol_resolve.replace_expr(axiom.upper_bound);
+  if(axiom.lower_bound)
+    symbol_resolve.replace_expr(*axiom.lower_bound);
 }
 
-extern inline string_constraintt &to_string_constraint(exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
-  return static_cast<string_constraintt &>(expr);
-}
+exprt univ_within_bounds(const string_constraintt &axiom);
 
 /// Used for debug printing.
 /// \param [in] ns: namespace for `from_expr`
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline std::string to_string(const string_constraintt &expr)
-{
-  std::ostringstream out;
-  out << "forall " << format(expr.univ_var()) << " in ["
-      << format(expr.lower_bound()) << ", " << format(expr.upper_bound())
-      << "). " << format(expr.premise()) << " => " << format(expr.body());
-  return out.str();
-}
+std::string to_string(const string_constraintt &expr);
+
+/// Checks the data invariant for string_constraintt
+/// \param stream : output stream
+/// \param [in] ns: namespace for `from_expr`
+/// \param [in] constraint: the string constraint to check
+/// \return whether the constraint satisfies the invariant
+bool is_valid_string_constraint(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const string_constraintt &constraint);
 
 /// Constraints to encode non containement of strings.
-class string_not_contains_constraintt : public exprt
+class string_not_contains_constraintt final : public exprt
 {
 public:
   // string_not contains_constraintt are formula of the form:
@@ -209,38 +164,11 @@ class string_not_contains_constraintt : public exprt
 /// \param [in] identifier: identifier for `from_expr`
 /// \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();
-}
+std::string to_string(const string_not_contains_constraintt &expr);
 
-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);
-}
+const string_not_contains_constraintt &
+to_string_not_contains_constraint(const exprt &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);
-}
+string_not_contains_constraintt &to_string_not_contains_constraint(exprt &expr);
 
 #endif
diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp
index ca555921144..57aa2dfb2b9 100644
--- a/src/solvers/refinement/string_constraint_generator_comparison.cpp
+++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp
@@ -43,8 +43,10 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
-  string_constraintt a2(
-    qvar, s1.length(), implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
+  string_constraintt a2;
+  a2.univ_var = qvar;
+  a2.upper_bound = s1.length();
+  a2.body = implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar]));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
@@ -131,7 +133,10 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     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(), implies_exprt(eq, constr2));
+  string_constraintt a2;
+  a2.univ_var = qvar;
+  a2.upper_bound = s1.length();
+  a2.body = implies_exprt(eq, constr2);
   constraints.push_back(a2);
 
   const symbol_exprt witness =
@@ -224,8 +229,10 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   lemmas.push_back(a1);
 
   const symbol_exprt i = fresh_univ_index("QA_compare_to", index_type);
-  const string_constraintt a2(
-    i, s1.length(), implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
+  string_constraintt a2;
+  a2.univ_var = i;
+  a2.upper_bound = s1.length();
+  a2.body = implies_exprt(res_null, equal_exprt(s1[i], s2[i]));
   constraints.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
@@ -255,8 +262,10 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   lemmas.push_back(a3);
 
   const symbol_exprt i2 = fresh_univ_index("QA_compare_to", index_type);
-  const string_constraintt a4(
-    i2, x, implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
+  string_constraintt a4;
+  a4.univ_var = i2;
+  a4.upper_bound = x;
+  a4.body = implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
   constraints.push_back(a4);
 
   return res;
diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp
index fa38ac46bc1..beebc0b360a 100644
--- a/src/solvers/refinement/string_constraint_generator_concat.cpp
+++ b/src/solvers/refinement/string_constraint_generator_concat.cpp
@@ -55,13 +55,19 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   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]));
+  string_constraintt a3;
+  a3.univ_var = idx;
+  a3.upper_bound = s1.length();
+  a3.body = equal_exprt(s1[idx], res[idx]);
   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);
+  string_constraintt a4;
+  a4.univ_var = idx2;
+  a4.upper_bound = minus_exprt(end_index, start_index);
+  a4.body = res_eq;
   constraints.push_back(a4);
 
   // We should have a enum type for the possible error codes
@@ -90,7 +96,10 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   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]));
+  string_constraintt a2;
+  a2.univ_var = idx;
+  a2.upper_bound = s1.length();
+  a2.body = equal_exprt(s1[idx], res[idx]);
   constraints.push_back(a2);
 
   equal_exprt a3(res[s1.length()], c);
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index e2336e598a9..1cf063e369f 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -64,16 +64,19 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
     binary_relation_exprt(from_index, ID_le, zero), zero, from_index);
 
   symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
-  string_constraintt a4(
-    n, lower_bound, index, implies_exprt(contains, notequal_exprt(str[n], c)));
+  string_constraintt a4;
+  a4.univ_var = n;
+  a4.lower_bound = lower_bound;
+  a4.upper_bound = index;
+  a4.body = implies_exprt(contains, not_exprt(equal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
-  string_constraintt a5(
-    m,
-    lower_bound,
-    str.length(),
-    implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
+  string_constraintt a5;
+  a5.univ_var = m;
+  a5.lower_bound = lower_bound;
+  a5.upper_bound = str.length();
+  a5.body = implies_exprt(not_exprt(contains), notequal_exprt(str[m], c));
   constraints.push_back(a5);
 
   return index;
@@ -126,11 +129,11 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   lemmas.push_back(a2);
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
-  string_constraintt a3(
-    qvar,
-    needle.length(),
-    implies_exprt(
-      contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
+  string_constraintt a3;
+  a3.univ_var = qvar;
+  a3.upper_bound = needle.length();
+  a3.body = implies_exprt(
+    contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
   constraints.push_back(a3);
 
   // string_not contains_constraintt are formulas of the form:
@@ -220,8 +223,10 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
-  const string_constraintt a3(
-    qvar, needle.length(), implies_exprt(contains, constr3));
+  string_constraintt a3;
+  a3.univ_var = qvar;
+  a3.upper_bound = needle.length();
+  a3.body = implies_exprt(contains, constr3);
   constraints.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
@@ -360,18 +365,18 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
     str.length());
 
   const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
-  const string_constraintt a4(
-    n,
-    plus_exprt(index, index1),
-    end_index,
-    implies_exprt(contains, notequal_exprt(str[n], c)));
+  string_constraintt a4;
+  a4.univ_var = n;
+  a4.lower_bound = plus_exprt(index, index1);
+  a4.upper_bound = end_index;
+  a4.body = implies_exprt(contains, notequal_exprt(str[n], c));
   constraints.push_back(a4);
 
   const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
-  const string_constraintt a5(
-    m,
-    end_index,
-    implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
+  string_constraintt a5;
+  a5.univ_var = m;
+  a5.upper_bound = end_index;
+  a5.body = implies_exprt(not_exprt(contains), notequal_exprt(str[m], c));
   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 a739aa18efe..0bee16cb8e1 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -369,7 +369,11 @@ void string_constraint_generatort::add_constraint_on_characters(
   const and_exprt char_in_set(
     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, char_in_set);
+  string_constraintt sc;
+  sc.univ_var = qvar;
+  sc.lower_bound = start;
+  sc.upper_bound = end;
+  sc.body = char_in_set;
   constraints.push_back(sc);
 }
 
diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp
index 09948073b49..4100e098286 100644
--- a/src/solvers/refinement/string_constraint_generator_testing.cpp
+++ b/src/solvers/refinement/string_constraint_generator_testing.cpp
@@ -43,11 +43,11 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type);
-  string_constraintt a2(
-    qvar,
-    prefix.length(),
-    implies_exprt(
-      isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar])));
+  string_constraintt a2;
+  a2.univ_var = qvar;
+  a2.upper_bound = prefix.length();
+  a2.body = implies_exprt(
+    isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type);
@@ -152,10 +152,10 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
 
   symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
   const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
-  string_constraintt a2(
-    qvar,
-    s0.length(),
-    implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
+  string_constraintt a2;
+  a2.univ_var = qvar;
+  a2.upper_bound = s0.length();
+  a2.body = implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted]));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
@@ -222,10 +222,10 @@ exprt string_constraint_generatort::add_axioms_for_contains(
 
   symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
   const plus_exprt qvar_shifted(qvar, startpos);
-  string_constraintt a4(
-    qvar,
-    s1.length(),
-    implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
+  string_constraintt a4;
+  a4.univ_var = qvar;
+  a4.upper_bound = s1.length();
+  a4.body = implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
   constraints.push_back(a4);
 
   string_not_contains_constraintt a5(
diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index e4df62603fd..9f49a661353 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -51,16 +51,18 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
   lemmas.push_back(res.axiom_for_has_length(k));
 
   const symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
-  const string_constraintt a2(
-    idx, minimum(s1.length(), k), equal_exprt(s1[idx], res[idx]));
+  string_constraintt a2;
+  a2.univ_var = idx;
+  a2.upper_bound = minimum(s1.length(), k);
+  a2.body = equal_exprt(s1[idx], res[idx]);
   constraints.push_back(a2);
 
   symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type);
-  string_constraintt a3(
-    idx2,
-    s1.length(),
-    res.length(),
-    equal_exprt(res[idx2], constant_char(0, char_type)));
+  string_constraintt a3;
+  a3.univ_var = idx2;
+  a3.lower_bound = s1.length();
+  a3.upper_bound = res.length();
+  a3.body = equal_exprt(res[idx2], constant_char(0, char_type));
   constraints.push_back(a3);
 
   return from_integer(0, signedbv_typet(32));
@@ -138,10 +140,10 @@ exprt string_constraint_generatort::add_axioms_for_substring(
   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)]));
+  string_constraintt a4;
+  a4.univ_var = idx;
+  a4.upper_bound = res.length();
+  a4.body = equal_exprt(res[idx], str[plus_exprt(start, idx)]);
   constraints.push_back(a4);
   return from_integer(0, signedbv_typet(32));
 }
@@ -203,7 +205,10 @@ exprt string_constraint_generatort::add_axioms_for_trim(
 
   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);
+  string_constraintt a6;
+  a6.univ_var = n;
+  a6.upper_bound = idx;
+  a6.body = non_print;
   constraints.push_back(a6);
 
   symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type);
@@ -214,12 +219,18 @@ exprt string_constraint_generatort::add_axioms_for_trim(
     ID_le,
     space_char);
 
-  string_constraintt a7(n2, bound, eqn2);
+  string_constraintt a7;
+  a7.univ_var = n2;
+  a7.upper_bound = bound;
+  a7.body = eqn2;
   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);
+  string_constraintt a8;
+  a8.univ_var = n3;
+  a8.upper_bound = res.length();
+  a8.body = eqn3;
   constraints.push_back(a8);
 
   minus_exprt index_before(
@@ -302,7 +313,10 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case(
     binary_relation_exprt(str[idx], ID_lt, from_integer(0x100, char_type)));
   if_exprt conditional_convert(is_upper_case, converted, non_converted);
 
-  string_constraintt a2(idx, res.length(), conditional_convert);
+  string_constraintt a2;
+  a2.univ_var = idx;
+  a2.upper_bound = res.length();
+  a2.body = conditional_convert;
   constraints.push_back(a2);
 
   return from_integer(0, f.type());
@@ -349,7 +363,10 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   minus_exprt diff(char_A, char_a);
   equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff));
   implies_exprt body1(is_lower_case, convert);
-  string_constraintt a2(idx1, res.length(), body1);
+  string_constraintt a2;
+  a2.univ_var = idx1;
+  a2.upper_bound = res.length();
+  a2.body = body1;
   constraints.push_back(a2);
 
   symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type);
@@ -359,7 +376,10 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
       binary_relation_exprt(str[idx2], ID_le, char_z)));
   equal_exprt eq(res[idx2], str[idx2]);
   implies_exprt body2(is_not_lower_case, eq);
-  string_constraintt a3(idx2, res.length(), body2);
+  string_constraintt a3;
+  a3.univ_var = idx2;
+  a3.upper_bound = res.length();
+  a3.body = body2;
   constraints.push_back(a3);
   return from_integer(0, signedbv_typet(32));
 }
@@ -416,14 +436,18 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
   lemmas.push_back(a2);
 
   const symbol_exprt q = fresh_univ_index("QA_char_set", position.type());
-  const equal_exprt a3_body(res[q], str[q]);
-  const string_constraintt a3(q, minimum(res.length(), position), a3_body);
+  string_constraintt a3;
+  a3.univ_var = q;
+  a3.upper_bound = minimum(res.length(), position);
+  a3.body = equal_exprt(res[q], str[q]);
   constraints.push_back(a3);
 
   const symbol_exprt q2 = fresh_univ_index("QA_char_set2", position.type());
-  const plus_exprt lower_bound(position, from_integer(1, position.type()));
-  const equal_exprt a4_body(res[q2], str[q2]);
-  const string_constraintt a4(q2, lower_bound, res.length(), a4_body);
+  string_constraintt a4;
+  a4.univ_var = q2;
+  a4.lower_bound = plus_exprt(position, from_integer(1, position.type()));
+  a4.upper_bound = res.length();
+  a4.body = equal_exprt(res[q2], str[q2]);
   constraints.push_back(a4);
 
   return if_exprt(
@@ -500,7 +524,10 @@ exprt string_constraint_generatort::add_axioms_for_replace(
     implies_exprt case2(
       not_exprt(equal_exprt(str[qvar], old_char)),
       equal_exprt(res[qvar], str[qvar]));
-    string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
+    string_constraintt a2;
+    a2.univ_var = qvar;
+    a2.upper_bound = res.length();
+    a2.body = and_exprt(case1, case2);
     constraints.push_back(a2);
     return from_integer(0, f.type());
   }
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 53da9d1cbb6..961ca51d9d4 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -29,11 +29,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <unordered_set>
 
-static bool is_valid_string_constraint(
-  messaget::mstreamt &stream,
-  const namespacet &ns,
-  const string_constraintt &expr);
-
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
   ui_message_handlert::uit ui,
@@ -718,7 +713,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     constraints.end(),
     std::back_inserter(axioms.universal),
     [&](string_constraintt constraint) { // NOLINT
-      symbol_resolve.replace_expr(constraint);
+      replace(constraint, symbol_resolve);
       DATA_INVARIANT(
         is_valid_string_constraint(error(), ns, constraint),
         string_refinement_invariantt(
@@ -1398,8 +1393,8 @@ static exprt negation_of_not_contains_constraint(
 static exprt negation_of_constraint(const string_constraintt &axiom)
 {
   // If the for all is vacuously true, the negation is false.
-  const exprt &lb=axiom.lower_bound();
-  const exprt &ub=axiom.upper_bound();
+  const exprt &lb = axiom.get_lower_bound();
+  const exprt &ub = axiom.upper_bound;
   if(lb.id()==ID_constant && ub.id()==ID_constant)
   {
     const auto lb_int = numeric_cast<mp_integer>(lb);
@@ -1410,11 +1405,11 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
 
   // If the premise is false, the implication is trivially true, so the
   // negation is false.
-  if(axiom.premise()==false_exprt())
+  if(axiom.index_guard == false_exprt())
     return false_exprt();
 
-  and_exprt premise(axiom.premise(), axiom.univ_within_bounds());
-  and_exprt negaxiom(premise, not_exprt(axiom.body()));
+  const and_exprt premise(axiom.index_guard, univ_within_bounds(axiom));
+  const and_exprt negaxiom(premise, not_exprt(axiom.body));
 
   return negaxiom;
 }
@@ -1461,34 +1456,22 @@ exprt concretize_arrays_in_expression(
 
 /// Debugging function which outputs the different steps an axiom goes through
 /// to be checked in check axioms.
+/// \tparam T: can be either string_constraintt, string_not_contains_constraintt
+template <typename T>
 static void debug_check_axioms_step(
   messaget::mstreamt &stream,
   const namespacet &ns,
-  const exprt &axiom,
-  const exprt &axiom_in_model,
+  const T &axiom,
+  const T &axiom_in_model,
   const exprt &negaxiom,
   const exprt &with_concretized_arrays)
 {
   static const std::string indent = "  ";
   static const std::string indent2 = "    ";
   stream << indent2 << "- axiom:\n" << indent2 << indent;
-
-  if(axiom.id() == ID_string_constraint)
-    stream << to_string(to_string_constraint(axiom));
-  else if(axiom.id() == ID_string_not_contains_constraint)
-    stream << to_string(to_string_not_contains_constraint(axiom));
-  else
-    stream << format(axiom);
+  stream << to_string(axiom);
   stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent;
-
-  if(axiom_in_model.id() == ID_string_constraint)
-    stream << to_string(to_string_constraint(axiom_in_model));
-  else if(axiom_in_model.id() == ID_string_not_contains_constraint)
-    stream << to_string(to_string_not_contains_constraint(axiom_in_model));
-  else
-    stream << format(axiom_in_model);
-
-  stream << '\n'
+  stream << to_string(axiom_in_model) << '\n'
          << indent2 << "- negated_axiom:\n"
          << indent2 << indent << format(negaxiom) << '\n';
   stream << indent2 << "- negated_axiom_with_concretized_arrays:\n"
@@ -1545,16 +1528,19 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   for(size_t i=0; i<axioms.universal.size(); i++)
   {
     const string_constraintt &axiom=axioms.universal[i];
-    const symbol_exprt &univ_var=axiom.univ_var();
-    const exprt &bound_inf=axiom.lower_bound();
-    const exprt &bound_sup=axiom.upper_bound();
-    const exprt &prem=axiom.premise();
+    const symbol_exprt &univ_var = axiom.univ_var;
+    const exprt &bound_inf = axiom.get_lower_bound();
+    const exprt &bound_sup = axiom.upper_bound;
+    const exprt &prem = axiom.index_guard;
     INVARIANT(
       prem == true_exprt(), "string constraint premises are not supported");
-    const exprt &body=axiom.body();
 
-    const string_constraintt axiom_in_model(
-      univ_var, get(bound_inf), get(bound_sup), get(body));
+    string_constraintt axiom_in_model;
+    axiom_in_model.univ_var = univ_var;
+    axiom_in_model.lower_bound = get(bound_inf);
+    axiom_in_model.upper_bound = get(bound_sup);
+    axiom_in_model.index_guard = get(prem);
+    axiom_in_model.body = get(axiom.body);
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
     negaxiom = simplify_expr(negaxiom, ns);
@@ -1648,13 +1634,13 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         const exprt &val=v.second;
         const string_constraintt &axiom=axioms.universal[v.first];
 
-        implies_exprt instance(axiom.premise(), axiom.body());
-        replace_expr(axiom.univ_var(), val, instance);
+        implies_exprt instance(axiom.index_guard, axiom.body);
+        replace_expr(axiom.univ_var, val, instance);
         // We are not sure the index set contains only positive numbers
         and_exprt bounds(
-          axiom.univ_within_bounds(),
+          univ_within_bounds(axiom),
           binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
-        replace_expr(axiom.univ_var(), val, bounds);
+        replace_expr(axiom.univ_var, val, bounds);
         const implies_exprt counter(bounds, instance);
         lemmas.push_back(counter);
       }
@@ -1857,32 +1843,14 @@ static exprt compute_inverse_function(
   return sum_over_map(elems, f.type(), neg);
 }
 
-class find_qvar_visitort : public const_expr_visitort
-{
-private:
-  const exprt &qvar_;
-
-public:
-  bool found;
-
-  explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {}
-
-  void operator()(const exprt &expr) override
-  {
-    if(expr==qvar_)
-      found=true;
-  }
-};
-
 /// look for the symbol and return true if it is found
 /// \param index: an index expression
 /// \param qvar: a symbol expression
 /// \return a Boolean
 static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
 {
-  find_qvar_visitort v2(qvar);
-  index.visit(v2);
-  return v2.found;
+  return std::find(index.depth_begin(), index.depth_end(), qvar) !=
+         index.depth_end();
 }
 
 /// Add to the index set all the indices that appear in the formulas and the
@@ -2012,10 +1980,10 @@ static void initial_index_set(
   const namespacet &ns,
   const string_constraintt &axiom)
 {
-  const symbol_exprt &qvar=axiom.univ_var();
-  const auto &bound = axiom.upper_bound();
-  auto it = axiom.body().depth_begin();
-  const auto end = axiom.body().depth_end();
+  const symbol_exprt &qvar = axiom.univ_var;
+  const auto &bound = axiom.upper_bound;
+  auto it = axiom.body.depth_begin();
+  const auto end = axiom.body.depth_end();
   while(it != end)
   {
     if(it->id() == ID_index && is_char_type(it->type()))
@@ -2158,18 +2126,18 @@ static exprt instantiate(
   const exprt &str,
   const exprt &val)
 {
-  const optionalt<exprt> idx = find_index(axiom.body(), str, axiom.univ_var());
+  const optionalt<exprt> idx = find_index(axiom.body, str, axiom.univ_var);
   if(!idx.has_value())
     return true_exprt();
 
-  const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, *idx);
+  const exprt r = compute_inverse_function(stream, axiom.univ_var, val, *idx);
   implies_exprt instance(
     and_exprt(
-      binary_relation_exprt(axiom.univ_var(), ID_ge, axiom.lower_bound()),
-      binary_relation_exprt(axiom.univ_var(), ID_lt, axiom.upper_bound()),
-      axiom.premise()),
-    axiom.body());
-  replace_expr(axiom.univ_var(), r, instance);
+      binary_relation_exprt(axiom.univ_var, ID_ge, axiom.get_lower_bound()),
+      binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound),
+      axiom.index_guard),
+    axiom.body);
+  replace_expr(axiom.univ_var, r, instance);
   return instance;
 }
 
@@ -2354,137 +2322,3 @@ static optionalt<exprt> find_counter_example(
   else
     return { };
 }
-
-/// \related string_constraintt
-typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
-
-/// \related string_constraintt
-static array_index_mapt gather_indices(const exprt &expr)
-{
-  array_index_mapt indices;
-  // clang-format off
-  std::for_each(
-    expr.depth_begin(),
-    expr.depth_end(),
-    [&](const exprt &expr)
-    {
-      const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
-      if(index_expr)
-        indices[index_expr->array()].push_back(index_expr->index());
-    });
-  // clang-format on
-  return indices;
-}
-
-/// \param expr: an expression
-/// \param var: a symbol
-/// \return Boolean telling whether `expr` is a linear function of `var`.
-/// \todo Add unit tests
-/// \related string_constraintt
-static bool
-is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
-{
-  for(auto it = expr.depth_begin(); it != expr.depth_end();)
-  {
-    if(
-      it->id() != ID_plus && it->id() != ID_minus &&
-      it->id() != ID_unary_minus && *it != var)
-    {
-      if(find_qvar(*it, var))
-        return false;
-      else
-        it.next_sibling_or_parent();
-    }
-    else
-      ++it;
-  }
-  return true;
-}
-
-/// The universally quantified variable is only allowed to occur in index
-/// expressions in the body of a string constraint. This function returns true
-/// if this is the case and false otherwise.
-/// \related string_constraintt
-/// \param [in] expr: The string constraint to check
-/// \return true if the universal variable only occurs in index expressions,
-///   false otherwise.
-static bool universal_only_in_index(const string_constraintt &expr)
-{
-  for(auto it = expr.body().depth_begin(); it != expr.body().depth_end();)
-  {
-    if(*it == expr.univ_var())
-      return false;
-    if(it->id() == ID_index)
-      it.next_sibling_or_parent();
-    else
-      ++it;
-  }
-  return true;
-}
-
-/// Checks the data invariant for \link string_constraintt \endlink
-/// \related string_constraintt
-/// \param stream: message stream
-/// \param ns: namespace
-/// \param [in] expr: the string constraint to check
-/// \return whether the constraint satisfies the invariant
-static bool is_valid_string_constraint(
-  messaget::mstreamt &stream,
-  const namespacet &ns,
-  const string_constraintt &expr)
-{
-  const auto eom=messaget::eom;
-  // Condition 1: The premise cannot contain any string indices
-  const array_index_mapt premise_indices=gather_indices(expr.premise());
-  if(!premise_indices.empty())
-  {
-    stream << "Premise has indices: " << format(expr) << ", map: {";
-    for(const auto &pair : premise_indices)
-    {
-      stream << format(pair.first) << ": {";
-      for(const auto &i : pair.second)
-        stream << format(i) << ", ";
-    }
-    stream << "}}" << eom;
-    return false;
-  }
-
-  const array_index_mapt body_indices=gather_indices(expr.body());
-  // Must validate for each string. Note that we have an invariant that the
-  // second value in the pair is non-empty.
-  for(const auto &pair : body_indices)
-  {
-    // Condition 2: All indices of the same string must be the of the same form
-    const exprt rep=pair.second.back();
-    for(size_t j=0; j<pair.second.size()-1; j++)
-    {
-      const exprt i=pair.second[j];
-      const equal_exprt equals(rep, i);
-      const exprt result=simplify_expr(equals, ns);
-      if(result.is_false())
-      {
-        stream << "Indices not equal: " << format(expr)
-               << ", str: " << format(pair.first) << eom;
-        return false;
-      }
-    }
-
-    // Condition 3: f must be linear in the quantified variable
-    if(!is_linear_arithmetic_expr(rep, expr.univ_var()))
-    {
-      stream << "f is not linear: " << format(expr)
-             << ", str: " << format(pair.first) << eom;
-      return false;
-    }
-
-    // Condition 4: the quantified variable can only occur in indices in the
-    // body
-    if(!universal_only_in_index(expr))
-    {
-      stream << "Universal variable outside of index:" << format(expr) << eom;
-      return false;
-    }
-  }
-
-  return true;
-}
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 128f5b0a04f..0dc9cfbb29f 100644
--- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -204,7 +204,6 @@ SCENARIO("instantiate_not_contains",
       constraints.end(),
       axioms,
       [&](const std::string &accu, string_constraintt sc) { // NOLINT
-        simplify(sc, ns);
         return accu + from_expr(ns, "", sc) + "\n\n";
       });