diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 6279ec7f5aa..aeabd7e28ea 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -166,6 +166,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/string_builtin_function.cpp \
       refinement/string_refinement.cpp \
       refinement/string_refinement_util.cpp \
+      refinement/string_constraint.cpp \
       refinement/string_constraint_generator_code_points.cpp \
       refinement/string_constraint_generator_comparison.cpp \
       refinement/string_constraint_generator_concat.cpp \
diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp
new file mode 100644
index 00000000000..5fd34963693
--- /dev/null
+++ b/src/solvers/refinement/string_constraint.cpp
@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+ Module: String solver
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "string_constraint.h"
+
+#include <solvers/sat/satcheck.h>
+#include <util/symbol_table.h>
+
+/// Runs a solver instance to verify whether an expression can only be
+//  non-negative.
+/// \param expr: the expression to check for negativity
+/// \return true if `expr < 0` is unsatisfiable, false otherwise
+static bool cannot_be_neg(const exprt &expr)
+{
+  satcheck_no_simplifiert sat_check;
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  boolbvt solver(ns, sat_check);
+  const exprt zero = from_integer(0, expr.type());
+  const binary_relation_exprt non_neg(expr, ID_lt, zero);
+  solver << non_neg;
+  return solver() == decision_proceduret::resultt::D_UNSATISFIABLE;
+}
+
+string_constraintt::string_constraintt(
+  const symbol_exprt &_univ_var,
+  const exprt &lower_bound,
+  const exprt &upper_bound,
+  const exprt &body)
+  : univ_var(_univ_var),
+    lower_bound(lower_bound),
+    upper_bound(upper_bound),
+    body(body)
+{
+  INVARIANT(
+    cannot_be_neg(lower_bound),
+    "String constraints must have non-negative lower bound.\n" +
+      lower_bound.pretty());
+  INVARIANT(
+    cannot_be_neg(upper_bound),
+    "String constraints must have non-negative upper bound.\n" +
+      upper_bound.pretty());
+}
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index 3284faa6305..f92bce2211d 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -68,16 +68,10 @@ class string_constraintt final
   string_constraintt() = delete;
 
   string_constraintt(
-    symbol_exprt _univ_var,
-    exprt lower_bound,
-    exprt upper_bound,
-    exprt body)
-    : univ_var(_univ_var),
-      lower_bound(lower_bound),
-      upper_bound(upper_bound),
-      body(body)
-  {
-  }
+    const symbol_exprt &_univ_var,
+    const exprt &lower_bound,
+    const exprt &upper_bound,
+    const exprt &body);
 
   // Default bound inferior is 0
   string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 945cad667ec..ac2b081cde7 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -458,4 +458,5 @@ exprt length_constraint_for_insert(
   const array_string_exprt &s1,
   const array_string_exprt &s2);
 
+exprt zero_if_negative(const exprt &expr);
 #endif
diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp
index c71fcf1f6ae..7a9ae627b08 100644
--- a/src/solvers/refinement/string_constraint_generator_comparison.cpp
+++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp
@@ -39,26 +39,33 @@ exprt string_constraint_generatort::add_axioms_for_equals(
 
   typet index_type=s1.length().type();
 
-
-  implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  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])));
-  constraints.push_back(a2);
-
-  symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
-  exprt zero=from_integer(0, index_type);
-  and_exprt bound_witness(
-    binary_relation_exprt(witness, ID_lt, s1.length()),
-    binary_relation_exprt(witness, ID_ge, zero));
-  and_exprt witnessing(bound_witness, notequal_exprt(s1[witness], s2[witness]));
-  and_exprt diff_length(
-    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));
-  lemmas.push_back(a3);
+  // Axiom 1.
+  lemmas.push_back(implies_exprt(eq, equal_exprt(s1.length(), s2.length())));
+
+  // Axiom 2.
+  constraints.push_back([&] {
+    const symbol_exprt qvar = fresh_univ_index("QA_equal", index_type);
+    return string_constraintt(
+      qvar,
+      zero_if_negative(s1.length()),
+      implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
+  }());
+
+  // Axiom 3.
+  lemmas.push_back([&] {
+    const symbol_exprt witness =
+      fresh_exist_index("witness_unequal", index_type);
+    const exprt zero = from_integer(0, index_type);
+    const and_exprt bound_witness(
+      binary_relation_exprt(witness, ID_lt, s1.length()),
+      binary_relation_exprt(witness, ID_ge, zero));
+    const and_exprt witnessing(
+      bound_witness, notequal_exprt(s1[witness], s2[witness]));
+    const and_exprt diff_length(
+      notequal_exprt(s1.length(), s2.length()),
+      equal_exprt(witness, from_integer(-1, index_type)));
+    return implies_exprt(not_exprt(eq), or_exprt(diff_length, witnessing));
+  }());
 
   return tc_eq;
 }
@@ -132,7 +139,8 @@ 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));
+  const string_constraintt a2(
+    qvar, zero_if_negative(s1.length()), implies_exprt(eq, constr2));
   constraints.push_back(a2);
 
   const symbol_exprt witness =
@@ -226,7 +234,9 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   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])));
+    i,
+    zero_if_negative(s1.length()),
+    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);
@@ -257,7 +267,9 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   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])));
+    i2,
+    zero_if_negative(x),
+    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 3a8cdfca8cc..80091433c70 100644
--- a/src/solvers/refinement/string_constraint_generator_concat.cpp
+++ b/src/solvers/refinement/string_constraint_generator_concat.cpp
@@ -50,20 +50,21 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
     length_constraint_for_concat_substr(res, s1, s2, start_index, end_index));
 
   // Axiom 2.
-  constraints.push_back([&] { // NOLINT
+  constraints.push_back([&] {
     const symbol_exprt idx =
       fresh_univ_index("QA_index_concat", res.length().type());
-    return string_constraintt(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
+    return string_constraintt(
+      idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
   }());
 
   // Axiom 3.
-  constraints.push_back([&] { // NOLINT
+  constraints.push_back([&] {
     const symbol_exprt idx2 =
       fresh_univ_index("QA_index_concat2", res.length().type());
     const equal_exprt res_eq(
       res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
     const minus_exprt upper_bound(res.length(), s1.length());
-    return string_constraintt(idx2, upper_bound, res_eq);
+    return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
   }());
 
   return from_integer(0, get_return_code_type());
@@ -120,7 +121,8 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   lemmas.push_back(length_constraint_for_concat_char(res, s1));
 
   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(
+    idx, zero_if_negative(s1.length()), 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 6ac23094b05..6366b57ccdd 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -59,20 +59,21 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
       equal_exprt(str[index], c)));
   lemmas.push_back(a3);
 
-  const auto zero = from_integer(0, index_type);
-  const if_exprt lower_bound(
-    binary_relation_exprt(from_index, ID_le, zero), zero, from_index);
+  const exprt lower_bound(zero_if_negative(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)));
+    n,
+    lower_bound,
+    zero_if_negative(index),
+    implies_exprt(contains, notequal_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(),
+    zero_if_negative(str.length()),
     implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
   constraints.push_back(a5);
 
@@ -128,7 +129,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   string_constraintt a3(
     qvar,
-    needle.length(),
+    zero_if_negative(needle.length()),
     implies_exprt(
       contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
   constraints.push_back(a3);
@@ -221,7 +222,7 @@ 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));
+    qvar, zero_if_negative(needle.length()), implies_exprt(contains, constr3));
   constraints.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
@@ -361,15 +362,15 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
   const string_constraintt a4(
     n,
-    plus_exprt(index, index1),
-    end_index,
+    zero_if_negative(plus_exprt(index, index1)),
+    zero_if_negative(end_index),
     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,
+    zero_if_negative(end_index),
     implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
   constraints.push_back(a5);
 
diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp
index 3eb9643105b..64e380db7f7 100644
--- a/src/solvers/refinement/string_constraint_generator_insert.cpp
+++ b/src/solvers/refinement/string_constraint_generator_insert.cpp
@@ -53,7 +53,9 @@ exprt string_constraint_generatort::add_axioms_for_insert(
   constraints.push_back([&] { // NOLINT
     const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
     return string_constraintt(
-      i, s2.length(), equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
+      i,
+      zero_if_negative(s2.length()),
+      equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
   }());
 
   // Axiom 4.
@@ -62,7 +64,7 @@ exprt string_constraint_generatort::add_axioms_for_insert(
     return string_constraintt(
       i,
       offset1,
-      s1.length(),
+      zero_if_negative(s1.length()),
       equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
   }());
 
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 3d5ef77c8ad..91ec22bb45a 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -324,7 +324,8 @@ 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);
+  const string_constraintt sc(
+    qvar, zero_if_negative(start), zero_if_negative(end), char_in_set);
   constraints.push_back(sc);
 }
 
@@ -627,3 +628,11 @@ exprt maximum(const exprt &a, const exprt &b)
 {
   return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
 }
+
+/// Returns a non-negative version of the argument.
+/// \param  expr: expression of which we want a non-negative version
+/// \return `max(0, expr)`
+exprt zero_if_negative(const exprt &expr)
+{
+  return maximum(from_integer(0, expr.type()), expr);
+}
diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp
index 9c2cfd8b1b9..03889531390 100644
--- a/src/solvers/refinement/string_constraint_generator_testing.cpp
+++ b/src/solvers/refinement/string_constraint_generator_testing.cpp
@@ -54,7 +54,8 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
     const symbol_exprt qvar = fresh_univ_index("QA_isprefix", index_type);
     const exprt body = implies_exprt(
       isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
-    return string_constraintt(qvar, prefix.length(), body);
+    return string_constraintt(
+      qvar, maximum(from_integer(0, index_type), prefix.length()), body);
   }());
 
   // Axiom 3.
@@ -169,7 +170,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
   string_constraintt a2(
     qvar,
-    s0.length(),
+    zero_if_negative(s0.length()),
     implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
   constraints.push_back(a2);
 
@@ -239,7 +240,7 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   const plus_exprt qvar_shifted(qvar, startpos);
   string_constraintt a4(
     qvar,
-    s1.length(),
+    zero_if_negative(s1.length()),
     implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
   constraints.push_back(a4);
 
diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index effcef775e6..75f9c115477 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -52,14 +52,16 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
 
   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]));
+    idx,
+    zero_if_negative(minimum(s1.length(), k)),
+    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(),
+    zero_if_negative(s1.length()),
+    zero_if_negative(res.length()),
     equal_exprt(res[idx2], constant_char(0, char_type)));
   constraints.push_back(a3);
 
@@ -131,7 +133,9 @@ exprt string_constraint_generatort::add_axioms_for_substring(
   constraints.push_back([&] {
     const symbol_exprt idx = fresh_univ_index("QA_index_substring", index_type);
     return string_constraintt(
-      idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
+      idx,
+      zero_if_negative(res.length()),
+      equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
   }());
 
   return from_integer(0, signedbv_typet(32));
@@ -193,7 +197,7 @@ 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(n, zero_if_negative(idx), non_print);
   constraints.push_back(a6);
 
   // Axiom 7.
@@ -202,12 +206,12 @@ exprt string_constraint_generatort::add_axioms_for_trim(
     const minus_exprt bound(minus_exprt(str.length(), idx), res.length());
     const binary_relation_exprt eqn2(
       str[plus_exprt(idx, plus_exprt(res.length(), n2))], ID_le, space_char);
-    return string_constraintt(n2, bound, eqn2);
+    return string_constraintt(n2, zero_if_negative(bound), eqn2);
   }());
 
   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(n3, zero_if_negative(res.length()), eqn3);
   constraints.push_back(a8);
 
   // Axiom 9.
@@ -291,7 +295,8 @@ 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(
+    idx, zero_if_negative(res.length()), conditional_convert);
   constraints.push_back(a2);
 
   return from_integer(0, f.type());
@@ -338,7 +343,7 @@ 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(idx1, zero_if_negative(res.length()), body1);
   constraints.push_back(a2);
 
   symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type);
@@ -348,7 +353,7 @@ 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(idx2, zero_if_negative(res.length()), body2);
   constraints.push_back(a3);
   return from_integer(0, signedbv_typet(32));
 }
@@ -406,13 +411,15 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
 
   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);
+  const string_constraintt a3(
+    q, minimum(zero_if_negative(res.length()), position), a3_body);
   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);
+  const string_constraintt a4(
+    q2, lower_bound, zero_if_negative(res.length()), a4_body);
   constraints.push_back(a4);
 
   return if_exprt(
@@ -489,7 +496,8 @@ 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(
+      qvar, zero_if_negative(res.length()), and_exprt(case1, case2));
     constraints.push_back(a2);
     return from_integer(0, f.type());
   }