Add non-negative length constraint earlier

Add non-negativeness constraint on string lengths before doing the first
iteration over the index set.

These constraints used to be added after that step, and some of the
length variables were missing these constraints.

This is made very visible by the upcoming changes to the way we deal
with string lengths.

Author: Joel Allred

src/solvers/strings/string_refinement.cpp

@@ -737,6 +737,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   for(const exprt &lemma : generator.constraints.existential)
     add_lemma(lemma);
 
+  // All generated strings should have non-negative length
+  for(const auto &string : generator.array_pool.created_strings())
+  {
+    add_lemma(binary_relation_exprt{
+      string.length(), ID_ge, from_integer(0, string.length_type())});
+  }
+
   // Initial try without index set
   const auto get = [this](const exprt &expr) { return this->get(expr); };
   dependencies.clean_cache();
@@ -776,13 +783,6 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   for(const auto &instance : initial_instances)
     add_lemma(instance);
 
-  // All generated strings should have non-negative length
-  for(const auto &string : generator.array_pool.created_strings())
-  {
-    add_lemma(binary_relation_exprt{
-      string.length(), ID_ge, from_integer(0, string.length_type())});
-  }
-
   while((loop_bound_--) > 0)
   {
     dependencies.clean_cache();