Merge pull request #4614 from allredj/string-non-neg-constr-before-solve

String solver: add non-negative length constraint before solving [TG-7439]

Author: tautschnig

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(greater_or_equal_to(
+      string.length(), 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();