Test for String.contains and very large strings

This tests string refinement is able to deal with very large strings in
string_not_contains_constraintt objects.

Author: romainbrenguier

regression/jbmc-strings/StringContains03/Test.class

@@ -0,0 +1,23 @@
+public class Test {
+    public static String check(String s) {
+        // Filter
+        if (s == null) {
+            return "Null string";
+        }
+        if (s.length() < 16_000_000) {
+            return "Too short";
+        }
+
+        // Act
+        boolean b1 = s.contains("foobar");
+
+        // Filter output
+        if (b1) {
+            return "Contained";
+        }
+
+        // Assert
+        assert(false);
+        return "Unreachable";
+    }
+}

regression/jbmc-strings/StringContains03/Test.java

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --function Test.check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+file Test.java line 20 .*: FAILURE$
+--
+--
+--string-max-length is not used on purpose, because this tests the behaviour
+of string refinement on very large strings.