Correct add_constraints in string_dependencies

When the result of a function is not tested we don't need to add full
constraints, but constraints about the length may still be necessary as
the length field of the string can be accessed directly.

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -442,13 +442,15 @@ void string_dependenciest::add_constraints(
       for_each_successor(n, f);
     });
 
-  for(const auto &node : test_dependencies)
+  for(const auto &node : builtin_function_nodes)
   {
-    if(node.kind == node.BUILTIN)
+    if(test_dependencies.count(nodet(node)))
     {
       const auto &builtin = builtin_function_nodes[node.index];
       const exprt return_value = builtin.data->add_constraints(generator);
       generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
     }
+    else
+      generator.add_lemma(node.data->length_constraint());
   }
 }

src/solvers/refinement/string_refinement_util.h

@@ -238,6 +238,9 @@ class string_dependenciest
 
   void output_dot(std::ostream &stream) const;
 
+  /// For all builtin call on which a test (or an unsupported buitin)
+  /// result depends, add the corresponding constraints. For the other builtin
+  /// only add constraints on the length.
   void add_constraints(string_constraint_generatort &generatort);
 
 private: