String refinement: Do not fail if the solver returns a negative string length

The string length may initially be unconstrained, and such counterexamples
should not result in failing invariants. When enabling field sensitivity,
strings-smoke-tests/java_index_of2 was failing as the solver returned
-1073741820 for string_refinement#string_length#1 (which is a signed integer).

Author: tautschnig

src/solvers/strings/string_refinement.cpp

@@ -1213,6 +1213,12 @@ static exprt negation_of_not_contains_constraint(
 
   // The negated existential becomes an universal, and this is the unrolling of
   // that universal quantifier.
+  // Ff the upper bound is smaller than the lower bound (specifically, it might
+  // actually be negative as it is initially unconstrained) then there is
+  // nothing to do (and the reserve call would fail).
+  if(ube < lbe)
+    return and_exprt(univ_bounds, get(constraint.premise));
+
   std::vector<exprt> conjuncts;
   conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
   for(mp_integer i = lbe; i < ube; ++i)