Update regression test that can randomly fail

This test could randomly fail, it was simplified and the previous
version is marked as knownbug.
The problem should be corrected by PR 1420

regression/strings/StringIndexMethods04/StringIndexMethods04.java

@@ -1,6 +1,12 @@
 public class StringIndexMethods04
 {
    public static void main(String[] args)
+   {
+      String letters = "onatdiffblue";
+      assert letters.indexOf("diffblue")==2;
+   }
+
+  public static void mainBug(String[] args)
    {
       String letters = "automatictestcasegenerationatdiffblue";
       assert letters.indexOf("diffblue")==28;

regression/strings/StringIndexMethods04/test_bug.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+StringIndexMethods04.class
+--refine-strings --string-max-length 1000 --function StringIndexMethods04.mainBug
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion\.1\] .* line 6 .* FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This test can randomly fail because the solver does not come up with the right
+model on the first iteration and the constraint instatiation adds too many things.