Add tests for the use of string dependencies

This tests, check that only constraints for the string operation that
matters are added to the list of axioms of the string solver.
In the example added here, the solver would previously consider 11
constraints, but now only 3, and still finds the correct result.

Author: romainbrenguier

regression/jbmc-strings/StringDependencies/Test.class

@@ -0,0 +1,22 @@
+class Test {
+    void test(String s) {
+        // Filter
+        if(s == null)
+            return;
+
+        // Act
+
+        // this matters for the final test
+        String t = s.concat("_foo");
+
+        // these should be ignored by the solver as they
+        // do not matter for the final test
+        String u = s.concat("_bar");
+        String v = s.concat("_baz");
+        String w = s.concat("_fiz");
+        String x = s.concat("_buz");
+
+        // Assert
+        assert t.endsWith("foo");
+    }
+}

regression/jbmc-strings/StringDependencies/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 Test.class --function Test.test
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 20 .*: SUCCESS
+string_refinement::check_axioms: 3 universal axioms
+--
+--
+We check there are exactly 3 universal formulas considered by the solver (2 for
+`t = s.concat("_foo")` and 1 for `t.endsWith("foo")`).
+The other concatenations should be ignored.