[string-refinement] Allow index set saturation if

not_contains_constraints are present

In the case of not_contains_constraints, the fixpoint of the index set
may not be enough to ensure the model is correct.
Therefore we allow continuing even if the index set does not grow,
progress is ensured in that case by the addition of counter-examples.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -600,11 +600,15 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
       if(index_sets.current.empty())
       {
-        error() << "dec_solve: current index set is empty, "
-                << "this should not happen" << eom;
-        return resultt::D_ERROR;
+        if(axioms.not_contains.empty())
+        {
+          error() << "dec_solve: current index set is empty, "
+                  << "this should not happen" << eom;
+          return resultt::D_ERROR;
+        }
+        else
+          debug() << "dec_solve: current index set is empty" << eom;
       }
-
       current_constraints.clear();
       for(const auto &instance :
         generate_instantiations(