Corrections to the string solver

regression/strings/java_case/test.desc

@@ -3,8 +3,8 @@ test_case.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$
-^\[assertion.2\] assertion at file test_case.java line 12: SUCCESS$
-^\[assertion.3\] assertion at file test_case.java line 13: SUCCESS$
-^\[assertion.4\] assertion at file test_case.java line 14: FAILURE$
+^\[.*assertion.1\].* line 11.* SUCCESS$
+^\[.*assertion.2\].* line 12.* SUCCESS$
+^\[.*assertion.3\].* line 13.* SUCCESS$
+^\[.*assertion.4\].* line 14.* FAILURE$
 --

regression/strings/java_char_array/test.desc

@@ -3,7 +3,7 @@ test_char_array.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_char_array.java line 11: SUCCESS$
-^\[assertion.2\] assertion at file test_char_array.java line 12: SUCCESS$
-^\[assertion.3\] assertion at file test_char_array.java line 13: FAILURE$
+^\[.*assertion.1\].* line 11.* SUCCESS$
+^\[.*assertion.2\].* line 12.* SUCCESS$
+^\[.*assertion.3\].* line 13.* FAILURE$
 --

regression/strings/java_char_array_init/test.desc

@@ -3,9 +3,9 @@ test_init.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_init.java line 16: SUCCESS$
-^\[assertion.2\] assertion at file test_init.java line 17: SUCCESS$
-^\[assertion.3\] assertion at file test_init.java line 18: SUCCESS$
-^\[assertion.4\] assertion at file test_init.java line 20: SUCCESS$
-^\[assertion.5\] assertion at file test_init.java line 21: FAILURE$
+^\[.*assertion.1\].* line 16.* SUCCESS$
+^\[.*assertion.2\].* line 17.* SUCCESS$
+^\[.*assertion.3\].* line 18.* SUCCESS$
+^\[.*assertion.4\].* line 20.* SUCCESS$
+^\[.*assertion.5\].* line 21.* FAILURE$
 --

regression/strings/java_char_at/test.desc

@@ -3,7 +3,7 @@ test_char_at.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$
-^\[assertion.2\] assertion at file test_char_at.java line 13: FAILURE$
-^\[assertion.3\] assertion at file test_char_at.java line 15: SUCCESS$
+^\[.*assertion.1\].* line 11.* SUCCESS$
+^\[.*assertion.2\].* line 13.* FAILURE$
+^\[.*assertion.3\].* line 15.* SUCCESS$
 --

regression/strings/java_code_point/test.desc

@@ -3,9 +3,9 @@ test_code_point.class
 --string-refine
 ^EXIT=0$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$
-^\[assertion.2\] assertion at file test_code_point.java line 6: SUCCESS$
-^\[assertion.3\] assertion at file test_code_point.java line 7: SUCCESS$
-^\[assertion.4\] assertion at file test_code_point.java line 8: SUCCESS$
-^\[assertion.5\] assertion at file test_code_point.java line 11: SUCCESS$
+^\[.*assertion.1\].* line 5.* SUCCESS$
+^\[.*assertion.2\].* line 6.* SUCCESS$
+^\[.*assertion.3\].* line 7.* SUCCESS$
+^\[.*assertion.4\].* line 8.* SUCCESS$
+^\[.*assertion.5\].* line 11.* SUCCESS$
 --

regression/strings/java_compare/test.desc

@@ -3,8 +3,8 @@ test_compare.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$
-^\[assertion.2\] assertion at file test_compare.java line 8: FAILURE$
-^\[assertion.3\] assertion at file test_compare.java line 11: SUCCESS$
-^\[assertion.4\] assertion at file test_compare.java line 12: FAILURE$
+^\[.*assertion.1\].* line 6.* SUCCESS$
+^\[.*assertion.2\].* line 8.* FAILURE$
+^\[.*assertion.3\].* line 11.* SUCCESS$
+^\[.*assertion.4\].* line 12.* FAILURE$
 --

regression/strings/java_concat/test.desc

@@ -3,6 +3,6 @@ test_concat.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$
-^\[assertion.2\] assertion at file test_concat.java line 10: FAILURE$
+^\[.*assertion.1\].* line 9.* SUCCESS$
+^\[.*assertion.2\].* line 10.* FAILURE$
 --

regression/strings/java_contains/test.desc

@@ -3,6 +3,6 @@ test_contains.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$
-^\[assertion.2\] assertion at file test_contains.java line 8: FAILURE$
+^\[.*assertion.1\].* line 7.* SUCCESS$
+^\[.*assertion.2\].* line 8.* FAILURE$
 --

regression/strings/java_delete/test.desc

@@ -3,6 +3,6 @@ test_delete.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$
-^\[assertion.2\] assertion at file test_delete.java line 12: FAILURE$
+^\[.*assertion.1\].* line 11.* SUCCESS$
+^\[.*assertion.2\].* line 12.* FAILURE$
 --

regression/strings/java_easychair/test.desc

@@ -3,5 +3,5 @@ easychair.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$
+^\[.*assertion.1\].* line 29.* FAILURE$
 --

regression/strings/java_empty/test.desc

@@ -3,6 +3,6 @@ test_empty.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$
-^\[assertion.2\] assertion at file test_empty.java line 5: FAILURE$
+^\[.*assertion.1\].* line 4.* SUCCESS$
+^\[.*assertion.2\].* line 5.* FAILURE$
 --

regression/strings/java_equal/test.desc

@@ -3,6 +3,6 @@ test_equal.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$
-^\[assertion.2\] assertion at file test_equal.java line 8: SUCCESS$
+^\[.*assertion.1\].* line 7.* FAILURE$
+^\[.*assertion.2\].* line 8.* SUCCESS$
 --

regression/strings/java_float/test.desc

@@ -3,8 +3,8 @@ test_float.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$
-^\[assertion.2\] assertion at file test_float.java line 15: SUCCESS$
-^\[assertion.3\] assertion at file test_float.java line 16: SUCCESS$
-^\[assertion.4\] assertion at file test_float.java line 17: FAILURE$
+^\[.*assertion.1\].* line 14.* SUCCESS$
+^\[.*assertion.2\].* line 15.* SUCCESS$
+^\[.*assertion.3\].* line 16.* SUCCESS$
+^\[.*assertion.4\].* line 17.* FAILURE$
 --

regression/strings/java_index_of/test.desc

@@ -3,14 +3,14 @@ test_index_of.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$
-^\[assertion.2\] assertion at file test_index_of.java line 14: FAILURE$
-^\[assertion.3\] assertion at file test_index_of.java line 17: SUCCESS$
-^\[assertion.4\] assertion at file test_index_of.java line 18: FAILURE$
-^\[assertion.5\] assertion at file test_index_of.java line 21: SUCCESS$
-^\[assertion.6\] assertion at file test_index_of.java line 22: FAILURE$
-^\[assertion.7\] assertion at file test_index_of.java line 25: SUCCESS$
-^\[assertion.8\] assertion at file test_index_of.java line 26: FAILURE$
-^\[assertion.9\] assertion at file test_index_of.java line 28: SUCCESS$
-^\[assertion.10\] assertion at file test_index_of.java line 29: SUCCESS$
+^\[.*assertion.1\].* line 13.* SUCCESS$
+^\[.*assertion.2\].* line 14.* FAILURE$
+^\[.*assertion.3\].* line 17.* SUCCESS$
+^\[.*assertion.4\].* line 18.* FAILURE$
+^\[.*assertion.5\].* line 21.* SUCCESS$
+^\[.*assertion.6\].* line 22.* FAILURE$
+^\[.*assertion.7\].* line 25.* SUCCESS$
+^\[.*assertion.8\].* line 26.* FAILURE$
+^\[.*assertion.9\].* line 28.* SUCCESS$
+^\[.*assertion.10\].* line 29.* SUCCESS$
 --

regression/strings/java_int/test.desc

@@ -3,11 +3,11 @@ test_int.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$
-^\[assertion.2\] assertion at file test_int.java line 9: SUCCESS$
-^\[assertion.3\] assertion at file test_int.java line 12: SUCCESS$
-^\[assertion.4\] assertion at file test_int.java line 15: SUCCESS$
-^\[assertion.5\] assertion at file test_int.java line 18: SUCCESS$
-^\[assertion.6\] assertion at file test_int.java line 21: SUCCESS$
-^\[assertion.7\] assertion at file test_int.java line 23: FAILURE$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* SUCCESS$
+^\[.*assertion.3\].* line 12.* SUCCESS$
+^\[.*assertion.4\].* line 15.* SUCCESS$
+^\[.*assertion.5\].* line 18.* SUCCESS$
+^\[.*assertion.6\].* line 21.* SUCCESS$
+^\[.*assertion.7\].* line 23.* FAILURE$
 --

regression/strings/java_intern/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_intern.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+--

regression/strings/java_intern/test_intern.java

@@ -0,0 +1,10 @@
+public class test_intern {
+
+  public static void main(/*String[] argv*/) {
+    String s1 = "abc";
+	  String s3 = "abc";
+    String x = s1.intern();
+    String y = s3.intern();
+	  assert(x == y);
+  }
+}

regression/strings/java_noarg/test.desc

@@ -0,0 +1,9 @@
+FUTURE
+test_noarg.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 9.* SUCCESS$
+^\[.*assertion.2\].* line 10.* FAILURE$
+^\[.*assertion.3\].* line 11.* SUCCESS$
+--

regression/strings/java_noarg/test_noarg.java

@@ -0,0 +1,13 @@
+public class test_noarg {
+
+  public static void main(/* NO ARGUMENT*/) {
+    String s = new String("Hello World!");
+    char c = s.charAt(4);
+    StringBuilder sb = new StringBuilder(s);
+    sb.setCharAt(5,'-');
+    s = sb.toString();
+    assert(c == 'o');
+    assert(c == 'p');
+    assert(s.equals("Hello-World!"));
+  }
+}

regression/strings/java_parseint/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_parseint.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 6.* SUCCESS$
+^\[.*assertion.2\].* line 7.* FAILURE$
+--

regression/strings/java_parseint/test_parseint.java

@@ -0,0 +1,9 @@
+public class test_parseint {
+
+  public static void main(String[] argv) {
+    String twelve = new String("12");
+    int parsed = Integer.parseInt(twelve);
+    assert(parsed == 12);
+    assert(parsed != 12);
+  }
+}

regression/strings/java_prefix/test.desc

@@ -3,8 +3,8 @@ test_prefix.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$
-^\[assertion.2\] assertion at file test_prefix.java line 16: FAILURE$
-^\[assertion.3\] assertion at file test_prefix.java line 18: SUCCESS$
-^\[assertion.4\] assertion at file test_prefix.java line 20: FAILURE$
+^\[.*assertion.1\].* line 14.* SUCCESS$
+^\[.*assertion.2\].* line 16.* FAILURE$
+^\[.*assertion.3\].* line 18.* SUCCESS$
+^\[.*assertion.4\].* line 20.* FAILURE$
 --

regression/strings/java_replace/test.desc

@@ -3,6 +3,6 @@ test_replace.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$
-^\[assertion.2\] assertion at file test_replace.java line 8: FAILURE$
+^\[.*assertion.1\].* line 6.* SUCCESS$
+^\[.*assertion.2\].* line 8.* FAILURE$
 --

regression/strings/java_set_length/test.desc

@@ -3,7 +3,7 @@ test_set_length.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$
-^\[assertion.2\] assertion at file test_set_length.java line 9: SUCCESS$
-^\[assertion.3\] assertion at file test_set_length.java line 10: FAILURE$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* SUCCESS$
+^\[.*assertion.3\].* line 10.* FAILURE$
 --

regression/strings/java_string_builder/test.desc

@@ -3,7 +3,7 @@ test_string_builder.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$
-^\[assertion.2\] assertion at file test_string_builder.java line 12: SUCCESS$
-^\[assertion.3\] assertion at file test_string_builder.java line 13: FAILURE$
+^\[.*assertion.1\].* line 11.* SUCCESS$
+^\[.*assertion.2\].* line 12.* SUCCESS$
+^\[.*assertion.3\].* line 13.* FAILURE$
 --

regression/strings/java_string_builder_insert/test.desc

@@ -3,6 +3,6 @@ test_insert.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_insert.java line 17: SUCCESS$
-^\[assertion.2\] assertion at file test_insert.java line 18: FAILURE$
+^\[.*assertion.1\].* line 17.* SUCCESS$
+^\[.*assertion.2\].* line 18.* FAILURE$
 --

regression/strings/java_string_builder_length/test.desc

@@ -3,6 +3,6 @@ test_sb_length.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-\[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$
-\[assertion.2\] assertion at file test_sb_length.java line 8: FAILURE$
+\[.*assertion.1\].* line 6.* SUCCESS$
+\[.*assertion.2\].* line 8.* FAILURE$
 --

regression/strings/java_strlen/test.desc

@@ -3,6 +3,6 @@ test_length.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$
-^\[assertion.2\] assertion at file test_length.java line 11: FAILURE$
+^\[.*assertion.1\].* line 10.* SUCCESS$
+^\[.*assertion.2\].* line 11.* FAILURE$
 --

regression/strings/java_substring/test.desc

@@ -3,8 +3,8 @@ test_substring.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$
-^\[assertion.2\] assertion at file test_substring.java line 13: FAILURE$
-^\[assertion.3\] assertion at file test_substring.java line 20: SUCCESS$
-^\[assertion.4\] assertion at file test_substring.java line 21: FAILURE$
+^\[.*assertion.1\].* line 12.* SUCCESS$
+^\[.*assertion.2\].* line 13.* FAILURE$
+^\[.*assertion.3\].* line 20.* SUCCESS$
+^\[.*assertion.4\].* line 21.* FAILURE$
 --

regression/strings/java_suffix/test.desc

@@ -3,6 +3,6 @@ test_suffix.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$
-^\[assertion.2\] assertion at file test_suffix.java line 13: FAILURE$
+^\[.*assertion.1\].* line 12.* SUCCESS$
+^\[.*assertion.2\].* line 13.* FAILURE$
 --

regression/strings/java_trim/test.desc

@@ -3,6 +3,6 @@ test_trim.class
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$
-^\[assertion.2\] assertion at file test_trim.java line 6: FAILURE$
+^\[.*assertion.1\].* line 5.* SUCCESS$
+^\[.*assertion.2\].* line 6.* FAILURE$
 --