From f2c4804fc900e755bb9e05cd32badafeada4b030 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@cs.ox.ac.uk>
Date: Wed, 21 Dec 2016 14:51:01 +0000
Subject: [PATCH] Regression test for the string-refine option

We are going to add a string-refine option to CBMC, (instead a pass
option as used in previous version of the tests).
We changed the test description file accordingly and added a few
extra tests (for java char arrays).

Also changed the flag in string regression from CORE to FUTURE:
Since the string solver is not yet part of this branch, we mark the
tests for string functions as FUTURE. They will be changed to CORE
once the corresponding features are integrated in CBMC.
I also changed the Makefile for being able to test tests marked as
future.
---
 regression/strings/Makefile                   |   5 +++-
 regression/strings/cprover-string-hack.h      |   6 ++---
 regression/strings/java_case/test.desc        |   4 +--
 regression/strings/java_char_array/test.desc  |   9 +++++++
 .../java_char_array/test_char_array.class     | Bin 0 -> 820 bytes
 .../java_char_array/test_char_array.java      |  15 ++++++++++++
 .../strings/java_char_array_init/test.desc    |  11 +++++++++
 .../java_char_array_init/test_init.class      | Bin 0 -> 1209 bytes
 .../java_char_array_init/test_init.java       |  23 ++++++++++++++++++
 regression/strings/java_char_at/test.desc     |   4 +--
 regression/strings/java_code_point/test.desc  |   4 +--
 regression/strings/java_compare/test.desc     |   4 +--
 regression/strings/java_concat/test.desc      |   4 +--
 regression/strings/java_contains/test.desc    |   4 +--
 regression/strings/java_delete/test.desc      |   4 +--
 regression/strings/java_easychair/test.desc   |   4 +--
 regression/strings/java_empty/test.desc       |   4 +--
 regression/strings/java_equal/test.desc       |   4 +--
 regression/strings/java_float/test.desc       |   4 +--
 regression/strings/java_index_of/test.desc    |   4 +--
 regression/strings/java_int/test.desc         |   4 +--
 regression/strings/java_prefix/test.desc      |   4 +--
 regression/strings/java_replace/test.desc     |   4 +--
 regression/strings/java_set_length/test.desc  |   4 +--
 .../strings/java_string_builder/test.desc     |   4 +--
 .../java_string_builder_insert/test.desc      |   8 ++++++
 .../test_insert.class                         | Bin 0 -> 1049 bytes
 .../test_insert.java                          |  20 +++++++++++++++
 .../java_string_builder_length/test.desc      |   4 +--
 regression/strings/java_strlen/test.desc      |   4 +--
 regression/strings/java_substring/test.desc   |   4 +--
 regression/strings/java_suffix/test.desc      |   4 +--
 regression/strings/java_trim/test.desc        |   4 +--
 regression/strings/test1/test.c               |   4 +--
 regression/strings/test1/test.desc            |   4 +--
 regression/strings/test2/test.desc            |   4 +--
 regression/strings/test3.1/test.desc          |   4 +--
 regression/strings/test3.2/test.desc          |   4 +--
 regression/strings/test3.3/test.c             |   2 +-
 regression/strings/test3.3/test.desc          |   4 +--
 regression/strings/test3.4/test.desc          |   4 +--
 regression/strings/test3/test.c               |   2 +-
 regression/strings/test3/test.desc            |  12 ++++-----
 regression/strings/test4/test.c               |   2 +-
 regression/strings/test4/test.desc            |   4 +--
 regression/strings/test5/test.desc            |   4 +--
 regression/strings/test_char_set/test.desc    |   8 +++---
 regression/strings/test_concat/test.c         |   4 +--
 regression/strings/test_concat/test.desc      |   8 +++---
 regression/strings/test_contains/test.desc    |   4 +--
 regression/strings/test_equal/test.desc       |   8 +++---
 regression/strings/test_index_of/test.c       |   2 +-
 regression/strings/test_index_of/test.desc    |   4 +--
 regression/strings/test_int/test.c            |   4 +--
 regression/strings/test_int/test.desc         |  10 ++++----
 regression/strings/test_pass1/test.desc       |   4 +--
 regression/strings/test_pass_pc3/test.desc    |   8 +++---
 regression/strings/test_prefix/test.desc      |   4 +--
 regression/strings/test_strlen/test.desc      |   4 +--
 regression/strings/test_substring/test.desc   |  12 ++++-----
 regression/strings/test_suffix/test.desc      |   8 +++---
 61 files changed, 210 insertions(+), 121 deletions(-)
 create mode 100644 regression/strings/java_char_array/test.desc
 create mode 100644 regression/strings/java_char_array/test_char_array.class
 create mode 100644 regression/strings/java_char_array/test_char_array.java
 create mode 100644 regression/strings/java_char_array_init/test.desc
 create mode 100644 regression/strings/java_char_array_init/test_init.class
 create mode 100644 regression/strings/java_char_array_init/test_init.java
 create mode 100644 regression/strings/java_string_builder_insert/test.desc
 create mode 100644 regression/strings/java_string_builder_insert/test_insert.class
 create mode 100644 regression/strings/java_string_builder_insert/test_insert.java

diff --git a/regression/strings/Makefile b/regression/strings/Makefile
index 545b36925ac..f9aee8c563e 100644
--- a/regression/strings/Makefile
+++ b/regression/strings/Makefile
@@ -1,3 +1,6 @@
 
 test:
-	../test.pl -c ../../../src/cbmc/cbmc
+	@../test.pl -c ../../../src/cbmc/cbmc
+
+testfuture:
+	@../test.pl -c ../../../src/cbmc/cbmc -F
diff --git a/regression/strings/cprover-string-hack.h b/regression/strings/cprover-string-hack.h
index 9160e935529..1ec17bca535 100644
--- a/regression/strings/cprover-string-hack.h
+++ b/regression/strings/cprover-string-hack.h
@@ -56,7 +56,7 @@ typedef unsigned char __CPROVER_char;
  ******************************************************************************/
 extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2);
-extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func();
+extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func(char * str);
 extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func();
 extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2);
 extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str);
@@ -68,5 +68,5 @@ extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __
 extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
-extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
-extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i);
+extern int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
+extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int i);
diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc
index 49ea16d56ff..9f48288c694 100644
--- a/regression/strings/java_case/test.desc
+++ b/regression/strings/java_case/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_case.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$
diff --git a/regression/strings/java_char_array/test.desc b/regression/strings/java_char_array/test.desc
new file mode 100644
index 00000000000..8282b808b84
--- /dev/null
+++ b/regression/strings/java_char_array/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+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$
+--
diff --git a/regression/strings/java_char_array/test_char_array.class b/regression/strings/java_char_array/test_char_array.class
new file mode 100644
index 0000000000000000000000000000000000000000..836942da1346e6bee0164979a451b7eec1a18c9b
GIT binary patch
literal 820
zcmZuuOK%cU6#g#rxG)T5cvY~i(pnWL79X`S+87CHLPF~TV`95#F2kfwg~7}WCi+vl
zF~)^!HKB=`y4U}to;%tS8#m{id!FC--S0m?9|5?5YX%I=#W8PS0q3MSpFkXCjzt4H
z<~WuNT);BNMTXq62m;3s-H{jEcLUKIIDH1T&7g0%o*Uj}P%70Y3~FoCcNo$g*K@YU
z!=B?mmd#Wc3fE(pt?YF6#Y@o`2yd^^4Sm<!yCVlv-B8%iH^qynpW_n8WsV9*l_9=i
z5B^>;x}&jgI}csCGaouZxNAQX{;u$S@oH6WHj%;%!4W;1R+y+^#Y7!fOeA446sOml
z$CMuU{>UfLr`B<-nrPrEgEbv`)Z2ILkQDh3kAE8faASz=w4`Y>B*RgQur?)B5~Na<
z6<xw_(n7V;uF^X_J=GeJ=p<R+30&XlpTH%h!Z8&{@og;9pBeO_%qmKP6e%DzF+(;@
zuLbgqyjD8|`yd-(k=3IlLjoCODVD825CbPa%*Hw^6DXS*cI&ILRoB+m)tYkswpP-V
z3DkA{BeVl#>PPw;B)>p^dI<h4%4G|xWuH!#3u=KnO9kB$Z;>VU`rUL+LW)I@Y7q~O
z@ax2h6N5N%1h7c?GI3iYc5Pxdph}LW=ArzeB<IL;6gXx%&M=CIZGMSnizgb~jK~7n
g9O4rs4#3s-P?b;6rq_=Jk()KdQum~6r3l>F-+08D+W-In

literal 0
HcmV?d00001

diff --git a/regression/strings/java_char_array/test_char_array.java b/regression/strings/java_char_array/test_char_array.java
new file mode 100644
index 00000000000..3cfd4000d3a
--- /dev/null
+++ b/regression/strings/java_char_array/test_char_array.java
@@ -0,0 +1,15 @@
+public class test_char_array {
+
+    public static void main(String[] argv)
+    {
+        String s = "abc";
+        char [] str = s.toCharArray();
+        int[] test = new int[312];
+        char c = str[2];
+        String t = argv[0];
+        char d = t.charAt(0);
+        assert(str.length == 3);
+        assert(c == 'c');
+        assert(c == d || d < 'a' || d > 'z' );
+    }
+}
diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc
new file mode 100644
index 00000000000..fe5ffae7238
--- /dev/null
+++ b/regression/strings/java_char_array_init/test.desc
@@ -0,0 +1,11 @@
+FUTURE
+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$
+--
diff --git a/regression/strings/java_char_array_init/test_init.class b/regression/strings/java_char_array_init/test_init.class
new file mode 100644
index 0000000000000000000000000000000000000000..be3baee56bd4f0a276d7b18454f832685f146dce
GIT binary patch
literal 1209
zcmZuxOH&g;5dJ2~W|C!rB_TXiPy{6qAPS=LP{9C#@~{e{1stp;jJUYT!tRDD|A9xZ
zaPg>Du_{<%>D{CL9gDJO!&@q;?w;;%db+>v+F$$MegNphtcqH+a<r)k;F=WIqi9D`
zMF%?NF(s|8C}QZ2phtSr95+;GXpP{eJoie`7r`x#eigTIhvP0oyv=Z3;drK9aK}v7
zShmCp16yPW51R$kyU!3zc06YYW$YEfP(5uH#B4FYESzT&Oo6;%78vT1OVew{rjfRc
z!fJZnbIii(ki1wq?-{u_Gse1)=NO<a7$U<t>ma{6Zx@}Mm@s9wDo?oHOBv~r*)-In
zfk8i;S^5X17~&Y#a1Zx69%vZBsD_8gNNY?(0(A_^q_8Yo!#E}w8jcf<9`-%%IJUzO
z5SE5VnA9+Z$8@x8hUif>98WY%W9C#XbIWTY=Mi=(L+>P)GO}MzdTL5qC#!zzdLmC;
z+C{=A%1oJd`YF-m5m~~>5799E>Q1{U;kpD_#Bm~dKE+{66jr_0{-~yCB1!*w)%6U=
zb6=P;a_&_*WwB8-EcXnc+}KbD0r;k26~){u;;!7-|0U2?9MhVyXrX8wR)lLhV&#Zs
z+5)dg0otZTw9uZ`(qc2cK@N$mAebCA$woRgk!GZo&Rww25{L^V!@iTof{VCBHbL1W
z6#4;wboIM3oeJuc*;Ggu*_5JN*;H5xuG`r?1Qt@e2+sIMNZCbbb_YsV3E{HhB}8@*
z-9~L!Of8{e8x?!d7Isnj^T1sK*VPYa-QBUO5~@$2Q(@&R^udsSE72H=)trv|{&xQn
zy4GC2zlB5O*6{<f@qpj>1Zv2ZjfSCuqZ$$7FG>WcXhsEn2{iPg3Ii0$K*u8CH;ChR
zh~qsWKM~8niRUKDQV(SxiyX}ym+4<u_t)1Ql=8~a0Q!BVfmj@|65`w7p^pd!zaV;C
U)ZsK_QU!s^5jnFKzvip|0BZvGvj6}9

literal 0
HcmV?d00001

diff --git a/regression/strings/java_char_array_init/test_init.java b/regression/strings/java_char_array_init/test_init.java
new file mode 100644
index 00000000000..5f4e220844c
--- /dev/null
+++ b/regression/strings/java_char_array_init/test_init.java
@@ -0,0 +1,23 @@
+public class test_init {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[10];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+	String s = new String(str);
+	String t = new String(str,1,2);
+
+	System.out.println(s);
+	System.out.println(s.length());
+	assert(s.startsWith("Hello"));
+	assert(s.length() == 10);
+	assert(t.equals("el"));
+	String u = String.valueOf(str,3,2);
+	assert(u.equals("lo"));
+	assert(s.equals("Hello") || !t.equals("el") || !u.equals("lo"));
+    }
+}
diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc
index babcc395bcf..6f206a0f22f 100644
--- a/regression/strings/java_char_at/test.desc
+++ b/regression/strings/java_char_at/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_char_at.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$
diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc
index 1543a327fa4..35ca0cd6f4b 100644
--- a/regression/strings/java_code_point/test.desc
+++ b/regression/strings/java_code_point/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_code_point.class
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$
diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc
index c500900a21e..517b208c3e4 100644
--- a/regression/strings/java_compare/test.desc
+++ b/regression/strings/java_compare/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_compare.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$
diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc
index c6c0b193e5b..8ef2898e0d7 100644
--- a/regression/strings/java_concat/test.desc
+++ b/regression/strings/java_concat/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_concat.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$
diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc
index ade6b433bf1..4e7a3bd4f7d 100644
--- a/regression/strings/java_contains/test.desc
+++ b/regression/strings/java_contains/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test_contains.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$
diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc
index 377ada44770..c6c608c0955 100644
--- a/regression/strings/java_delete/test.desc
+++ b/regression/strings/java_delete/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test_delete.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$
diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc
index bd68fd1f60a..8680af72c5a 100644
--- a/regression/strings/java_easychair/test.desc
+++ b/regression/strings/java_easychair/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 easychair.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$
diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc
index 56b21e2041c..cab514b80b5 100644
--- a/regression/strings/java_empty/test.desc
+++ b/regression/strings/java_empty/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_empty.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$
diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc
index 6375cfdc3d8..d66c30b26fe 100644
--- a/regression/strings/java_equal/test.desc
+++ b/regression/strings/java_equal/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_equal.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$
diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc
index 5edfd6eea22..955f0358eab 100644
--- a/regression/strings/java_float/test.desc
+++ b/regression/strings/java_float/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_float.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$
diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc
index dd5c60464d5..daa6c32493b 100644
--- a/regression/strings/java_index_of/test.desc
+++ b/regression/strings/java_index_of/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_index_of.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$
diff --git a/regression/strings/java_int/test.desc b/regression/strings/java_int/test.desc
index 5211656c61b..ae60dd78af0 100644
--- a/regression/strings/java_int/test.desc
+++ b/regression/strings/java_int/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_int.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$
diff --git a/regression/strings/java_prefix/test.desc b/regression/strings/java_prefix/test.desc
index b234bba1788..175f934ca1d 100644
--- a/regression/strings/java_prefix/test.desc
+++ b/regression/strings/java_prefix/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_prefix.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$
diff --git a/regression/strings/java_replace/test.desc b/regression/strings/java_replace/test.desc
index a5b15efd737..1e89ebe37b4 100644
--- a/regression/strings/java_replace/test.desc
+++ b/regression/strings/java_replace/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_replace.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$
diff --git a/regression/strings/java_set_length/test.desc b/regression/strings/java_set_length/test.desc
index 66cf52835ac..43f82a648fd 100644
--- a/regression/strings/java_set_length/test.desc
+++ b/regression/strings/java_set_length/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_set_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$
diff --git a/regression/strings/java_string_builder/test.desc b/regression/strings/java_string_builder/test.desc
index c0b3b6a51ce..9712205b104 100644
--- a/regression/strings/java_string_builder/test.desc
+++ b/regression/strings/java_string_builder/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_string_builder.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$
diff --git a/regression/strings/java_string_builder_insert/test.desc b/regression/strings/java_string_builder_insert/test.desc
new file mode 100644
index 00000000000..2655f846da1
--- /dev/null
+++ b/regression/strings/java_string_builder_insert/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+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$
+--
diff --git a/regression/strings/java_string_builder_insert/test_insert.class b/regression/strings/java_string_builder_insert/test_insert.class
new file mode 100644
index 0000000000000000000000000000000000000000..69a32d7f93fa8cbebd4e1f6c84f79c41463bb3b1
GIT binary patch
literal 1049
zcmZuwT~8B16g|_Aop!sWYg<1206|e&3RFc<DI!obm;g#@HNb;e+6gXhcX4;C@u$ci
z@L5bsB1YeQ@JA8vv_Sdr<<9J#bI+V}=kDLbAHM*MV?l+EevW|%Zm0<0rVN8J+=}8h
zhE!ybjiLj?5#&^iV3cD_g(hqAD(>Je$32GBpy7GK^-ah27EI6Bv_zGGturXorfvE&
z48ctHHAATAR0Ts~$+X2vy|yXbR}xGIHN&(Sx-uI}+r~#DZyEMhzT~^6y;YEf@se*;
z-Y*+FO+3dqY38`k5Sgx6M^~sNr|wq7GgA`kzVQ6FrY&WSNlFbVq#3%;)6dsUt14WQ
z+W*OMt*XRLXqdzU4G-~%V@g8-(;SaA%*c~VNHWA0g=IOd3eutB31%63+T?S`4SDLi
z4zb5h>EW2uFpnasY!|%P+!hs|A+T{a-)aIwXXgK%QCc1u`ZCWqirEXGBYy>ImG2yr
zr85_Sgg7Oq^x5-8jo!_vlc>%Xt?A@n(v$c^Ba9jqq?-EArWyE-1X=W+iuh1BEbpB9
zmeoR*<|EN=K+&Qhq7kSH&vZrgq=EGEew_|zg4QuWv#8VPGQCGW1nq(#8Awy?q_19D
z8Li>reXws5h%SmsGszG|H+pC<p?|0}M5`J38D7c-^~G{7q>FMctXt)rA_Lc*@&N*C
z$>2Uh%Ok;D1K~F#4Ja#n;G+#h_7L4gdNipv5ZguU0NUC<;=fO)zqHd*PM|4g5^>sx
z>3W4Eaq<))4^fh)l7l#gC^Lox{h&Ig$mc3KeMgAPRFy#B5UU(lIIePB>!Q-$6Z;cQ
kpFlE&js_CD;GwSw1-~QOzWlfsk}Qlsd{%a>uc__&KWVw%^#A|>

literal 0
HcmV?d00001

diff --git a/regression/strings/java_string_builder_insert/test_insert.java b/regression/strings/java_string_builder_insert/test_insert.java
new file mode 100644
index 00000000000..1fac897c5ed
--- /dev/null
+++ b/regression/strings/java_string_builder_insert/test_insert.java
@@ -0,0 +1,20 @@
+public class test_insert {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[5];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+
+
+	StringBuilder sb = new StringBuilder(" world");
+	sb.insert(0,str);
+	String s = sb.toString();
+	System.out.println(s);
+	assert(s.equals("Hello world"));
+	assert(!s.equals("Hello world"));
+    }
+}
diff --git a/regression/strings/java_string_builder_length/test.desc b/regression/strings/java_string_builder_length/test.desc
index a15660ee85b..c4720992571 100644
--- a/regression/strings/java_string_builder_length/test.desc
+++ b/regression/strings/java_string_builder_length/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_sb_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 \[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$
diff --git a/regression/strings/java_strlen/test.desc b/regression/strings/java_strlen/test.desc
index 78007186493..b98e6f76f0a 100644
--- a/regression/strings/java_strlen/test.desc
+++ b/regression/strings/java_strlen/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_length.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$
diff --git a/regression/strings/java_substring/test.desc b/regression/strings/java_substring/test.desc
index 78a9bcca9cb..bd54a8204fe 100644
--- a/regression/strings/java_substring/test.desc
+++ b/regression/strings/java_substring/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_substring.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$
diff --git a/regression/strings/java_suffix/test.desc b/regression/strings/java_suffix/test.desc
index f9472f03b47..2740e87d6e4 100644
--- a/regression/strings/java_suffix/test.desc
+++ b/regression/strings/java_suffix/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_suffix.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$
diff --git a/regression/strings/java_trim/test.desc b/regression/strings/java_trim/test.desc
index fa0e10a1ca7..7c0f1a87978 100644
--- a/regression/strings/java_trim/test.desc
+++ b/regression/strings/java_trim/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test_trim.class
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$
diff --git a/regression/strings/test1/test.c b/regression/strings/test1/test.c
index d3830e38a3f..c5e10eb1fc7 100644
--- a/regression/strings/test1/test.c
+++ b/regression/strings/test1/test.c
@@ -5,13 +5,13 @@
 int main()
 {
     __CPROVER_string s;
-    __CPROVER_char c1, c2;
+    char c1, c2;
     int i;
     int j;
     i = 2;
     s = __CPROVER_string_literal("pippo");
     c1 = __CPROVER_char_at(s, i);
-    c2 = __CPROVER_char_literal("p");
+    c2 = 'p';
     assert (c1 == c2);
     assert (c1 != c2);
     return 0;
diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc
index f622390356d..b86ded86c18 100644
--- a/regression/strings/test1/test.desc
+++ b/regression/strings/test1/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion c1 == c2: SUCCESS$
diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc
index d3054f813f1..b322a1d0d33 100644
--- a/regression/strings/test2/test.desc
+++ b/regression/strings/test2/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion n == 5: SUCCESS$
diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test3.1/test.desc
+++ b/regression/strings/test3.1/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test3.2/test.desc
+++ b/regression/strings/test3.2/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.3/test.c b/regression/strings/test3.3/test.c
index 35e25d82ee5..bef96c6cd4e 100644
--- a/regression/strings/test3.3/test.c
+++ b/regression/strings/test3.3/test.c
@@ -16,7 +16,7 @@ int main()
     // proving the assertions individually seems to be much faster
     //assert(__CPROVER_string_length(s) == i + 5);
     //assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s));
-    assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
+    assert(__CPROVER_char_at(s, i) == 'p');
 
     return 0;
 }
diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test3.3/test.desc
+++ b/regression/strings/test3.3/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc
index dbf3c40cfdb..d88e1c83744 100644
--- a/regression/strings/test3.4/test.desc
+++ b/regression/strings/test3.4/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test3/test.c b/regression/strings/test3/test.c
index 2fa4b22e017..cbfc398099e 100644
--- a/regression/strings/test3/test.c
+++ b/regression/strings/test3/test.c
@@ -14,7 +14,7 @@ int main()
 
     assert(__CPROVER_string_length(s) == i + 5);
     assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s));
-    assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
+    assert(__CPROVER_char_at(s, i) == 'p');
     assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s));
 
     return 0;
diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc
index 6cacec86a19..54e56188c1b 100644
--- a/regression/strings/test3/test.desc
+++ b/regression/strings/test3/test.desc
@@ -1,10 +1,10 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s) == i + 5: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.3\] assertion __CPROVER_uninterpreted_string_char_at_func(s, i) == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.4\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"p!o\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s) == i + 5: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$
+^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == .p.: SUCCESS$
+^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"p!o\"), s): FAILURE$
 --
diff --git a/regression/strings/test4/test.c b/regression/strings/test4/test.c
index d73324f8ef4..3c768717823 100644
--- a/regression/strings/test4/test.c
+++ b/regression/strings/test4/test.c
@@ -9,7 +9,7 @@ int main()
     int j;
     i = 2;
     s = __CPROVER_string_literal("pippo");
-    if (__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")) {
+    if (__CPROVER_char_at(s, i) == 'p') {
         j = 1;
     }
     assert(j == 1);
diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc
index 0f5bd6ccca7..c88a62b6704 100644
--- a/regression/strings/test4/test.desc
+++ b/regression/strings/test4/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc
index dbf3c40cfdb..d88e1c83744 100644
--- a/regression/strings/test5/test.desc
+++ b/regression/strings/test5/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc
index 8cf42dda8f3..589767e4b82 100644
--- a/regression/strings/test_char_set/test.desc
+++ b/regression/strings/test_char_set/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("apc")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("abc")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("apc")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("abc")): FAILURE$
 --
diff --git a/regression/strings/test_concat/test.c b/regression/strings/test_concat/test.c
index 007b9ca1b5c..923bffb46ae 100644
--- a/regression/strings/test_concat/test.c
+++ b/regression/strings/test_concat/test.c
@@ -10,7 +10,7 @@ int main()
   u =  __CPROVER_string_concat(s, t);
   __CPROVER_char c = __CPROVER_char_at(u,i);
 
-  assert(c  == __CPROVER_char_literal("p"));
-  assert(__CPROVER_char_at(u,2)  == __CPROVER_char_literal("p"));
+  assert(c  == 'p');
+  assert(__CPROVER_char_at(u,2)  == 'p');
   return 0;
 }
diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc
index e5d8b30d6da..c3f1ca2a65a 100644
--- a/regression/strings/test_concat/test.desc
+++ b/regression/strings/test_concat/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion c == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(u, 2) == __CPROVER_uninterpreted_char_literal_func(\"p\"): FAILURE$
+^\[main.assertion.1\] assertion c == .p.: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at(u,2) == .p.: FAILURE$
 --
diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc
index 8275425c548..fcf9694b31d 100644
--- a/regression/strings/test_contains/test.desc
+++ b/regression/strings/test_contains/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$
diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc
index 81ad6913856..d3cfd4f3747 100644
--- a/regression/strings/test_equal/test.desc
+++ b/regression/strings/test_equal/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"pippo\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"mippo\")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("pippo")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("mippo")): FAILURE$
 --
diff --git a/regression/strings/test_index_of/test.c b/regression/strings/test_index_of/test.c
index d64d3c2d66e..c182e7952ab 100644
--- a/regression/strings/test_index_of/test.c
+++ b/regression/strings/test_index_of/test.c
@@ -7,7 +7,7 @@ int main(){
   __CPROVER_string str;
   int firstSlash = __CPROVER_string_index_of(str,'/');
   //__CPROVER_char_literal("/"));
-  int lastSlash = __CPROVER_string_last_index_of(str,__CPROVER_char_literal("/"));
+  int lastSlash = __CPROVER_string_last_index_of(str,'/');
 
   __CPROVER_assume(__CPROVER_string_equal(str, __CPROVER_string_literal("abc/abc/abc")));
 
diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc
index 6d9ddbc6281..edc8e09c4ed 100644
--- a/regression/strings/test_index_of/test.desc
+++ b/regression/strings/test_index_of/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$
diff --git a/regression/strings/test_int/test.c b/regression/strings/test_int/test.c
index 3f8f8651783..28aa9c7e156 100644
--- a/regression/strings/test_int/test.c
+++ b/regression/strings/test_int/test.c
@@ -5,12 +5,12 @@
 int main()
 {
   __CPROVER_string s;
-  unsigned i = 10;
+  int i = 10;
   s = __CPROVER_string_of_int(123);
   assert(__CPROVER_char_at(s,0)  == '1');
   assert(__CPROVER_char_at(s,1)  == '2');
 
-  unsigned j = __CPROVER_parse_int(__CPROVER_string_literal("234"));
+  int j = __CPROVER_parse_int(__CPROVER_string_literal("234"));
 
   assert(j == 234);
   assert(j < 233 || __CPROVER_char_at(s,2)  == '4');
diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc
index e46e43ed936..a13b3dad852 100644
--- a/regression/strings/test_int/test.desc
+++ b/regression/strings/test_int/test.desc
@@ -1,10 +1,10 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 0) == .1.: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 1) == .2.: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_char_at(s,0) == .1.: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at(s,1) == .2.: SUCCESS$
 ^\[main.assertion.3\] assertion j == 234: SUCCESS$
-^\[main.assertion.4\] assertion j < 233 || __CPROVER_uninterpreted_string_char_at_func(s, 2) == .4.: FAILURE$
+^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at(s,2) == .4.: FAILURE$
 --
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
index 7548b6e91ef..4e7cd79fde4 100644
--- a/regression/strings/test_pass1/test.desc
+++ b/regression/strings/test_pass1/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): SUCCESS
diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc
index 88f4659c45d..0e64d9b84d1 100644
--- a/regression/strings/test_pass_pc3/test.desc
+++ b/regression/strings/test_pass_pc3/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s3) == 0: FAILURE$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_length_func(s3) < 2: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s3) == 0: FAILURE$
+^\[main.assertion.2\] assertion __CPROVER_string_length(s3) < 2: SUCCESS$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc
index 187565433e4..6c62a2fa466 100644
--- a/regression/strings/test_prefix/test.desc
+++ b/regression/strings/test_prefix/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion b: SUCCESS$
diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc
index a35e2499c9f..30c3f4066ed 100644
--- a/regression/strings/test_strlen/test.desc
+++ b/regression/strings/test_strlen/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$
diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc
index 327d5bbe1f2..6e2609d9cd3 100644
--- a/regression/strings/test_substring/test.desc
+++ b/regression/strings/test_substring/test.desc
@@ -1,10 +1,10 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cc\")): FAILURE$
-^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"bc\")): SUCCESS$
-^\[main.assertion.4\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cd")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cc")): FAILURE$
+^\[main.assertion.3\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("bc")): SUCCESS$
+^\[main.assertion.4\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("cd")): FAILURE$
 --
diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc
index e0e8af7704c..a6667cfbfcf 100644
--- a/regression/strings/test_suffix/test.desc
+++ b/regression/strings/test_suffix/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 test.c
---pass
+--string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"pp\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("po"),s): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s): FAILURE$
 --