From 95e1d9e79b730adf395f5ad5b7063213f12c8f63 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Jun 2018 18:03:02 +0100 Subject: [PATCH] Deduplicate string tests --- .../jbmc-strings/java_append_string/test.desc | 7 ---- .../test_append_string.class | Bin 1032 -> 0 bytes .../test_append_string.java | 14 -------- .../jbmc-strings/java_case/test.desc | 7 ---- .../jbmc-strings/java_case/test_case.class | Bin 839 -> 0 bytes .../jbmc-strings/java_case/test_case.java | 12 ------- .../jbmc-strings/java_char_array/test.desc | 7 ---- .../java_char_array/test_char_array.class | Bin 676 -> 0 bytes .../java_char_array/test_char_array.java | 13 -------- .../jbmc-strings/java_code_point/test.desc | 7 ---- .../java_code_point/test_code_point.class | Bin 941 -> 0 bytes .../java_code_point/test_code_point.java | 14 -------- .../jbmc-strings/java_contains/test.desc | 7 ---- .../java_contains/test_contains.class | Bin 671 -> 0 bytes .../java_contains/test_contains.java | 9 ------ .../java_delete_char_at/test.desc | 7 ---- .../test_delete_char_at.class | Bin 923 -> 0 bytes .../test_delete_char_at.java | 11 ------- .../jbmc-strings/java_endswith/test.desc | 7 ---- .../java_endswith/test_endswith.class | Bin 666 -> 0 bytes .../java_endswith/test_endswith.java | 9 ------ .../jbmc-strings/java_equal/test.desc | 7 ---- .../jbmc-strings/java_equal/test_equal.class | Bin 725 -> 0 bytes .../jbmc-strings/java_equal/test_equal.java | 9 ------ .../jbmc-strings/java_float/test.desc | 7 ---- .../jbmc-strings/java_float/test_float.class | Bin 1015 -> 0 bytes .../jbmc-strings/java_float/test_float.java | 17 ---------- .../jbmc-strings/java_hash_code/test.desc | 7 ---- .../java_hash_code/test_hash_code.class | Bin 602 -> 0 bytes .../java_hash_code/test_hash_code.java | 9 ------ .../jbmc-strings/java_index_of/test.desc | 7 ---- .../java_index_of/test_index_of.class | Bin 631 -> 0 bytes .../java_index_of/test_index_of.java | 10 ------ .../jbmc-strings/java_index_of_char/test.desc | 7 ---- .../test_index_of_char.class | Bin 614 -> 0 bytes .../test_index_of_char.java | 10 ------ .../java_insert_char_array/test.desc | 8 ----- .../test_insert_char_array.class | Bin 1416 -> 0 bytes .../test_insert_char_array.java | 30 ------------------ .../java_insert_multiple/test.desc | 7 ---- .../test_insert_multiple.class | Bin 979 -> 0 bytes .../test_insert_multiple.java | 11 ------- .../jbmc-strings/java_insert_string/test.desc | 7 ---- .../test_insert_string.class | Bin 897 -> 0 bytes .../test_insert_string.java | 10 ------ .../java_append_object/test.desc | 10 ------ .../test_append_object.class | Bin 992 -> 0 bytes .../test_append_object.java | 17 ---------- .../java_char_array_init/test.desc | 10 ------ .../java_char_array_init/test_init.class | Bin 1046 -> 0 bytes .../java_char_array_init/test_init.java | 21 ------------ .../java_compare/test.desc | 8 ----- .../java_compare/test_compare.class | Bin 623 -> 0 bytes .../java_compare/test_compare.java | 9 ------ .../strings-smoke-tests/java_concat/test.desc | 9 ------ .../java_concat/test_concat.class | Bin 847 -> 0 bytes .../java_concat/test_concat.java | 13 -------- .../strings-smoke-tests/java_delete/test.desc | 8 ----- .../java_delete/test_delete.class | Bin 856 -> 0 bytes .../java_delete/test_delete.java | 10 ------ .../strings-smoke-tests/java_empty/test.desc | 8 ----- .../java_empty/test_empty.class | Bin 571 -> 0 bytes .../java_empty/test_empty.java | 8 ----- .../java_insert_int/test.desc | 8 ----- .../java_insert_int/test_insert_int.class | Bin 866 -> 0 bytes .../java_insert_int/test_insert_int.java | 10 ------ 66 files changed, 443 deletions(-) delete mode 100644 jbmc/regression/jbmc-strings/java_append_string/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_append_string/test_append_string.class delete mode 100644 jbmc/regression/jbmc-strings/java_append_string/test_append_string.java delete mode 100644 jbmc/regression/jbmc-strings/java_case/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_case/test_case.class delete mode 100644 jbmc/regression/jbmc-strings/java_case/test_case.java delete mode 100644 jbmc/regression/jbmc-strings/java_char_array/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_char_array/test_char_array.class delete mode 100644 jbmc/regression/jbmc-strings/java_char_array/test_char_array.java delete mode 100644 jbmc/regression/jbmc-strings/java_code_point/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_code_point/test_code_point.class delete mode 100644 jbmc/regression/jbmc-strings/java_code_point/test_code_point.java delete mode 100644 jbmc/regression/jbmc-strings/java_contains/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_contains/test_contains.class delete mode 100644 jbmc/regression/jbmc-strings/java_contains/test_contains.java delete mode 100644 jbmc/regression/jbmc-strings/java_delete_char_at/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class delete mode 100644 jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java delete mode 100644 jbmc/regression/jbmc-strings/java_endswith/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_endswith/test_endswith.class delete mode 100644 jbmc/regression/jbmc-strings/java_endswith/test_endswith.java delete mode 100644 jbmc/regression/jbmc-strings/java_equal/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_equal/test_equal.class delete mode 100644 jbmc/regression/jbmc-strings/java_equal/test_equal.java delete mode 100644 jbmc/regression/jbmc-strings/java_float/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_float/test_float.class delete mode 100644 jbmc/regression/jbmc-strings/java_float/test_float.java delete mode 100644 jbmc/regression/jbmc-strings/java_hash_code/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.class delete mode 100644 jbmc/regression/jbmc-strings/java_hash_code/test_hash_code.java delete mode 100644 jbmc/regression/jbmc-strings/java_index_of/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_index_of/test_index_of.class delete mode 100644 jbmc/regression/jbmc-strings/java_index_of/test_index_of.java delete mode 100644 jbmc/regression/jbmc-strings/java_index_of_char/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.class delete mode 100644 jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java delete mode 100644 jbmc/regression/jbmc-strings/java_insert_char_array/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class delete mode 100644 jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java delete mode 100644 jbmc/regression/jbmc-strings/java_insert_multiple/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class delete mode 100644 jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java delete mode 100644 jbmc/regression/jbmc-strings/java_insert_string/test.desc delete mode 100644 jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.class delete mode 100644 jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_append_object/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_append_object/test_append_object.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_char_array_init/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_char_array_init/test_init.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_compare/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_compare/test_compare.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_compare/test_compare.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_concat/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_concat/test_concat.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_concat/test_concat.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete/test_delete.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_delete/test_delete.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_empty/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_empty/test_empty.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_empty/test_empty.java delete mode 100644 jbmc/regression/strings-smoke-tests/java_insert_int/test.desc delete mode 100644 jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.class delete mode 100644 jbmc/regression/strings-smoke-tests/java_insert_int/test_insert_int.java diff --git a/jbmc/regression/jbmc-strings/java_append_string/test.desc b/jbmc/regression/jbmc-strings/java_append_string/test.desc deleted file mode 100644 index cb881ab83d92..000000000000 --- a/jbmc/regression/jbmc-strings/java_append_string/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -FUTURE -test_append_string.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion.1\].* line 12.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class b/jbmc/regression/jbmc-strings/java_append_string/test_append_string.class deleted file mode 100644 index f2cb5cf8bea64858805fef9f4a7b85663a237736..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1032 zcmZ`%YfsZq7=F%f?Meru444;G5OFYIiYO|G+zkq9GNXYnq^xJ;VAsyJGx3j@$RF^t zm~4q8`rRKzd{4(%Ci>O#pr zE299GN#|l;%vh8xqtx>Fd zp6f9f7g;J;)3J_?4vw$(4|yqI=+AAni#3VQ%h@HGjWSIAE8s%TSwHg~7{yP1z$>&3 zwrr8CA#mx#O^o97HW(K7ygKXMT2g4@qkf9p5twCpU;};lF3$v|8tnFx&xNnAM({YtBn zUE8Ej)}bFGb%e~M(OpN+7j&HL%!Uc)d-BN%l;Fd-LyXl zr$M$Ea^=duG@tZpFqn{H;@yz<-M?xELhBW};!Hqz+Oup&1cm=APt^3xRHIK%#xUO% zuIY&Gv`=~fZ%6>W*FF~L6J+V9uuMT-8D(LRZR9D=)2c`_qd8g~gMF4noS_)=H|era zm{LE|(J*0KCkX8s;V~l5sv|_36k@wypd6#LY^Wo|k5F7OG(X8zjl>B05fUdz?v0W9 zAvHq2#v)Y8qtHk#4TVgpD3M}~cGf80L;`1tkper#rh;?9AmseiQ{DFoWR3I)nPVuC ZPl$xSLYc`-T9Kuq2fgc5Qg9J*E){dIB97^X@Ek3d>|@8j-?_BAR$UQ1R+rl)yA=kOKPLFQ;EOQ zQ*N9ADV0DfcYYKw8_`5?+1>ei=b71`zrLLVXydL24^~WmQ{xBL4XrJJ0$4Q*;5X^exHNonpgNRVtjgx3^bli{B zE1k@NV;Luegg6g<4hhEFE}@vGT?XoC9v-XS&`w7)cDTx_KWngEn(K9kygI_lAj)DD4Q5Qd zh5iSPC^0YS?UQ4SR8v$ zF`hRkFn3#a`(e|Zz}oo&`xLd-xiiLUEs$fB*Mo43;&(W2&LDnhVPh)1#?su4DI6vf zOyr`%ZSM1{!jUrQHyf6~lE5-)G#8g<4DBfwr&Zhu3a1d(Cs^iJ*z*n-=vvK&;Xl#? JuCQTX^$$Dod?f$? diff --git a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java b/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java deleted file mode 100644 index 5028f5afa4d7..000000000000 --- a/jbmc/regression/jbmc-strings/java_char_array/test_char_array.java +++ /dev/null @@ -1,13 +0,0 @@ -public class test_char_array -{ - public static void main() - { - String s = "abc"; - char [] str = s.toCharArray(); - char c = str[2]; - char a = s.charAt(0); - assert(str.length != 3 || - a != 'a' || - c != 'c'); - } -} diff --git a/jbmc/regression/jbmc-strings/java_code_point/test.desc b/jbmc/regression/jbmc-strings/java_code_point/test.desc deleted file mode 100644 index cda7f110aba5..000000000000 --- a/jbmc/regression/jbmc-strings/java_code_point/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_code_point.class ---refine-strings --string-max-length 1000 --function test_code_point.main -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.class deleted file mode 100644 index f2f5fbad63a60c992bb2f3c9ef2d15fb99700de0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 941 zcmZ8fOHUI~7(KV0>20S|C<8)Okb3jldjA*!kixMtL$VnKLU`mO}F{YsdS&nfHmodSSXXqZWd|!Bh?K=Kl+qX8VqQbz| z7-BQFV+XSg(cI`NgHm!Uf}wNKcErQ_&W7-wNHJaPShmBES`Mu8izTZT(i~T)MuzxI zx%$^eTXySSS=_f}P){KIV7*M1>owPQf{AVGrKRH(dKm_Xj`v<4e|;C?n-JgsgKru7 zq&i=RSmg8EYj#ap$Sa4K?Gk7Z*F{ketF#dhq8f~OghatNVx zp2P}?7s#bW7R9FP(ZD)dOv$ZFTQ#>3N)2~&(-%SURV$@WyDLApyry4?{Mz|TRa!Vh zZ$@ diff --git a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java b/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java deleted file mode 100644 index 266a05c1646e..000000000000 --- a/jbmc/regression/jbmc-strings/java_code_point/test_code_point.java +++ /dev/null @@ -1,14 +0,0 @@ -public class test_code_point -{ - public static void main() - { - String s = "!𐤇𐤄𐤋𐤋𐤅"; - StringBuilder sb = new StringBuilder(); - sb.appendCodePoint(0x10907); - assert(s.codePointAt(1) != 67847 || - s.codePointBefore(3) != 67847 || - s.codePointCount(1,5) < 2 || - s.offsetByCodePoints(1,2) < 3 || - s.charAt(1) != sb.charAt(0)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_contains/test.desc b/jbmc/regression/jbmc-strings/java_contains/test.desc deleted file mode 100644 index cfa99b27ba06..000000000000 --- a/jbmc/regression/jbmc-strings/java_contains/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_contains.class ---refine-strings --string-max-length 1000 --function test_contains.main -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 7.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.class b/jbmc/regression/jbmc-strings/java_contains/test_contains.class deleted file mode 100644 index 9bbccb03775ac6ea7b4ea53619317d2a13ed93aa..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 671 zcmY*XT~8B16g_vl-Q8{%TegB#L`90WC6O22AVgC2#i|cACgsIUw-a0_yE;4dzrY{h zSxsmniN5onG~QWlE6HT$&iy#&+&gpi`}+?7+t~CG;I@l99#(u$s9NlaY9(=X%QX25+8FnYan>L(dZwB-%H0Tk}qOY5o(#~_feW?uFResiO(WH z1yw@T*jpo!9B%crijzZT-ycLKxo>5@_$O_gHS#BX)KdS?zDJLm3et*#KR;k4`miBIh?8D z(daP;c#;QL;|B@&xu{w<&9GGfqoB(BBHvc|BtDDn3FwPSM9907I|(J!W~qHHwK&$e zgw+oV6WA}qV)rYYGt}Cf7jREezJ%AGp!CxqSvgV&o9!aYa9Dtgb^a7L*;5AnGQVPp p7rT~cG}}2fuo(ImD4)T#&tVt7!I@)D)ft>3tl+8X;Z{yr{{zCLg0BDo diff --git a/jbmc/regression/jbmc-strings/java_contains/test_contains.java b/jbmc/regression/jbmc-strings/java_contains/test_contains.java deleted file mode 100644 index 7c0d5304cd32..000000000000 --- a/jbmc/regression/jbmc-strings/java_contains/test_contains.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_contains -{ - public static void main() - { - String s = new String("Abc"); - String u = "bc"; - assert(!s.contains(u)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc b/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc deleted file mode 100644 index a61ab36b4b10..000000000000 --- a/jbmc/regression/jbmc-strings/java_delete_char_at/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_delete_char_at.class ---refine-strings --string-max-length 1000 --function test_delete_char_at.main -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 9.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class deleted file mode 100644 index 130e3d10f6c1fc4b451b5ce93a816a301c3171d7..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 923 zcmaJ<+int36kUhg48tH4XiKYjtqRl@snlB=BSlS&cu6oe_Jtf~PH^gU24{x;i~Rwg z)r1epSp^Z4WSsNuc?B16(Z5|v zB8?>(mla&WRS9JUDL=iUpo(P)*BJ6k+;xTH8MfsB>cSMB=xT4c)8*dkF5l-Wa>z5x`}dm3t$wZJIfm8W8XBf998%NlX)0DxlW<){ z9cwCXprIm*8HPwxBU%;fxJeunjAmHlL&vcRB>xY33Aa?-#vO+2QFFG ykrdcZ)Fl)pECiuYXCn{<%;eG|oH~FM`+!*VGvo<&sM*JfBck5-D?1%fpZN{e4a}GT diff --git a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java b/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java deleted file mode 100644 index ffb4f48a59c1..000000000000 --- a/jbmc/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java +++ /dev/null @@ -1,11 +0,0 @@ -public class test_delete_char_at -{ - public static void main() - { - StringBuilder s = new StringBuilder(); - s.append("Abc"); - org.cprover.CProverString.deleteCharAt(s, 1); - String str = s.toString(); - assert(!str.equals("Ac")); - } -} diff --git a/jbmc/regression/jbmc-strings/java_endswith/test.desc b/jbmc/regression/jbmc-strings/java_endswith/test.desc deleted file mode 100644 index 9aba187f2868..000000000000 --- a/jbmc/regression/jbmc-strings/java_endswith/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_endswith.class ---refine-strings --string-max-length 1000 --function test_endswith.main -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 7.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.class deleted file mode 100644 index e3d453c444f4c7dce39962d72b8d7b7035fe7911..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 666 zcmZ`%O;6iE5Pjn~w&NHQoC2W*T1pBbNO0j+R25NrX=o2YRN+!N_KGeIPGxV}-vWPt zGawPENc7(S)QVXb5^+FU?at1}dv9j<&%a+c05-7d!o!S>rw*REFfi+2t^gPF`tsby z3m1-#FSvM#MH@9jr52>ANR;fw={uPQovw%obU?5+Wh~VjLax5DPcXN8ksy?sG8P~E z#~qRE>0}NZ2Qns%wNwy(+YP>FZq`6>HpA{6hTH1(lTf^uy24i?RbNCLr9Y+mx^@)& z2t1TfCX}_k-VNfz^_EIxe8})yoiNhjR|G>_V;J|agk?f?l)ZJ|#7>g*5?1qo!baW0 z3K|axK6Q>ns0fqw<_PCM>ucSxqXm9ufsdr{h)Scv?Jm!eFcpbZCL$W@;i;%T2Y84F zSm3wt_@$^^)orkq1EZkK`vl+S_#{5_jRELfC&K65%AAA(D#O$^ml_lBs7>J{u06tCg52Ppj3NJfU_!(=fW-g+ diff --git a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java b/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java deleted file mode 100644 index 5e743a9c569b..000000000000 --- a/jbmc/regression/jbmc-strings/java_endswith/test_endswith.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_endswith -{ - public static void main() - { - String s = new String("Abcd"); - String suff = "cd"; - assert(!s.endsWith(suff)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_equal/test.desc b/jbmc/regression/jbmc-strings/java_equal/test.desc deleted file mode 100644 index bd4d1022d783..000000000000 --- a/jbmc/regression/jbmc-strings/java_equal/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_equal.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_equal/test_equal.class b/jbmc/regression/jbmc-strings/java_equal/test_equal.class deleted file mode 100644 index e0fc6db8aaf91eb799f5e02cfdd3194a232479f1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 725 zcmZuv(M}Ul5IwWq?rxXGEvx= z;+}l3G?kyqB>f~m4@B@UA9;WfY!zHDhgGcI;r`G)k-d~qsr`QtD{CydmoTo{tnGEuSY-?qZLNCyn? zP7krfPvh~!QL(BgU@r$|L6OfHzAdmNw)xc&=(|otiBBsF5(+5eA^SS@E0>yVcP?QZ zlyW1O?aa%ww_D2Z{eU$@d985)dx)t^I0qvX{*0rI=G~}PGBTxk)?#^X(_$qXbNu@> zS+~WJ3L`#@D>QA)j=u`SbGO}ZWNiX7CHDeTL)hjwn7N;@Cj2*(Xs$dA?~R_fn#n)9 E2H7QzvH$=8 diff --git a/jbmc/regression/jbmc-strings/java_equal/test_equal.java b/jbmc/regression/jbmc-strings/java_equal/test_equal.java deleted file mode 100644 index e8c9ac7cb1a4..000000000000 --- a/jbmc/regression/jbmc-strings/java_equal/test_equal.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_equal -{ - public static void main(String[] argv) - { - String s = new String("pi"); - String t = new String("po"); - assert(!s.equals(t)); - } -} diff --git a/jbmc/regression/jbmc-strings/java_float/test.desc b/jbmc/regression/jbmc-strings/java_float/test.desc deleted file mode 100644 index d79c25dab3aa..000000000000 --- a/jbmc/regression/jbmc-strings/java_float/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -THOROUGH -test_float.class ---refine-strings --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 15.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_float/test_float.class b/jbmc/regression/jbmc-strings/java_float/test_float.class deleted file mode 100644 index 00e8622e2ac6a2341fb02487fba698f9df054765..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1015 zcmZuw(Nfbu6g``!*)*iI1dFYxpn$d@R0UCKRS@WmGl)8Mbi@Y?ZD4|Ff=TKOPxu@1 z13s%W;OLC{jw=kk!)6dzerS7cuwVz~nq$=& z*b0MEwp}~C%@E5Mo-oMsUfp6yE!nQM+-$5_{$l~Ag@$Rn41M|MOPl6vv*?)aMzI?D zw!2Xh8-1(S|UpY>il2y=N-Bp z)ZDri*uGW&Q#tBs*rWxz8!L42Qgk5!md=WXP!t0beIwgPqch|g`S|EQ*n0uQNwP{b zNnJt~If@1J2PAOvFAQnHh%Fj&W#|*)GxD&o@eyH_4^VQ-9=P!Gp^ryi-9;g%7>PY- zZ!wUQjjkxl?5S{l>92mJw>~+UoK)T@a{v7{V8UuO3{K1-^M0#&>}c zLTOSaiHcL*jFNSo$XY|y3A9JZE$c|9KM3~B>|cVj)~qW+@3xNA@7768#k;1M6DLwf zgzjo8!{cA_Gz$xi67tJoi zm&l`!BL&biMg#)>I8RZ}Q zDmo;H!o}_ZVZ7NIApWI4EPmmJ2hpuAzZIbt%2XvX>^tGkvmPh-p*m>rQ`Au zd@F%nVubfm{+s5L_%xPoK$m$TD!iLTkWfaoU)q7jU|`PGzPhE>((*O*^(z=>s7&eS z7`lV`;|AhS&Y~48H5hz17-jM&Sl;4Em*H~M0X<+=V2l^f1~2+LtA#dDb**cZ&mi;* Y=%wE<2EkOZP&1R^$!B?%hXrN{9`a z#Cn_Uknuj|@Y;umK|;-@S35F3THSnZ_k%HsAyob+6L{le9&ZUjAGg~+R$=x}sF@iZ z9}z^}%I+b1S=?FLVUvB>R)^<9s75N)Mnye!cAIrM!NWP=Mg>nBprB^^krnVA(S2%sIkQ5A=k(K!x}>FxpdD%awtVinv4h62iHLQ~Uv^Py5`Q PrEyX4H>`!RTy^{pE-iAY diff --git a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java b/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java deleted file mode 100644 index 999b50f68960..000000000000 --- a/jbmc/regression/jbmc-strings/java_index_of_char/test_index_of_char.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_index_of_char -{ - public static void main() - { - String s = "Abc"; - char c = 'c'; - int i = s.indexOf(c); - assert(i != 2); - } -} diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc b/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc deleted file mode 100644 index 0fd3fc08bb06..000000000000 --- a/jbmc/regression/jbmc-strings/java_insert_char_array/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_insert_char_array.class ---refine-strings --string-max-length 1000 --function test_insert_char_array.main -^EXIT=10$ -^SIGNAL=0$ -assertion.* line 26.* SUCCESS$ -assertion.* line 28.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class b/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class deleted file mode 100644 index c19a742c0f4ddb43f1234627a0ee00cf490fecfb..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1416 zcmZuwSx*yD6#njXxn-Er(w2&V3JBVTQWso{3zS8aO%aG&$g~}Cv~=ps)WmoHggpA< zt71}&8h!WA_--P4?zFXml1c7z=A7?*=R4>A-23t!z!+9!L=fYM`;d?!At{y-v7}^# zFe)RBGd`RZmve16k1-h+aIuZ9mwdP^;|i{FWMl*d%D9YcxXy8dAv~m7mS)@4jXlc7=bx*u)O1lTZKhWomkfh{#a8n#7Sys6O!ZJ6y(9=QoQSnVOjh(_K{GRR z1SdFbsd|aF*j#*#<0i)hgKs=vtP_=2jEb4pW^_TT*VZh1qlUeaCu$q2;5I5qDL8^| zh9d_F*3&UScuXqDVoJd@W)$?Ik7HKB3EX0k)PgwmbId8YjXNCk3Km2_7ox;Z&E*S3 zPQfCU7`mHjCK_5#o2FrsPKT4^SXOWs_ZWiB*rnWaEl)B@kFxvhHEkKXTII_K(Y$K8 ztd*##eX&D&(omR$w2cN-Bz9=?jvD4>I$t)8SDKm5E<1Z8WVSVX1A4Bdt(jK%hV%Z? zUR$=dMH6ULsPL{Dj&7uvY2a+itf^ZxQ(;G={bmMU7EVPP7q9lRq86=q5DlLs_S=%)23-Hy>tGXzg! z7wn^OL=UZA$H>qohKbI?bptN?fZ?x@9)w)GaL>E0^(DT)LuWG4H&%sb{f)%l|NWJ$ z!ux?7B?l@>83mvWPF#FsgV`Nnz{ei-9oc%_aY&56!WGPDJCJ+C}XYj>DZ|XCA z>rH+g4ii5?cMwQ`LI*Hd58bJUK5=-q37(#Bo`n%tFtanT zw$ZZ#|2C4TP)8MkZ47=z@WC!Re>mny&HNVa4YQz9t8WzTbPiE{VImWuwTsk^;y9^% zl1>Q{Zg!ZE*K{xLu#%Z{}>Y RM__p%DK|wEPdSuM{{uprGQa=; diff --git a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java b/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java deleted file mode 100644 index f392655afc14..000000000000 --- a/jbmc/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java +++ /dev/null @@ -1,30 +0,0 @@ -public class test_insert_char_array -{ - // These are models of the String methods manipulating char arrays - public static String stringOfCharArray(char arr[]) - { - StringBuilder sb=new StringBuilder(""); - for(int i=0; i7KwMRE4I45F40CI`?{hD(T*rTG`Fg|VCIj1Lh*T`c3LY?o zvblE*;i_wLhIq|#_^VE=a6j0y95H&Y)v*JsZS#$N{Xo|+hZMu2xEE~QX%^~%XF1JB9m_Vk#~|sZ=(!=| zriNQ6lG=v2+}2RSriNK0NtE6&Oj4lX4(>9f$7~OW>pt;3m*`UeQzGM@hB7J)i81nZ zW1kzrU#WpKhWTu5+&4&;#iM0huURnKo_oN(LiJ5Q4l$9z_6(&-@X4~}=hfT<@vz45 z>=fVxtb7`i61YQIsqAE9ncToXbadPQXVt-zlyhX4`1k>;HhGF+!Q{T>adY(I_(P@-a)K#V?~<2xLd3=$xmoWr~dARK5rHSu|pS&PYGW5XIuCH6W-&wasHl zJIPQF;TQRE!Z^azc0Qbp96{dBccIk2AbN<@dQ$Bo_7SmTXgfVj{}AL-pL~hvX(CjL zNyu1&f)yH7qD-19F|c1K$;b>!XGRK&eO170a;A&;A>{BUghO8u9di$b3!W)R+Ll=F IY=89fA9A7H#sB~S diff --git a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java b/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java deleted file mode 100644 index e9ed16a8e91d..000000000000 --- a/jbmc/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java +++ /dev/null @@ -1,11 +0,0 @@ -public class test_insert_multiple -{ - public static void main() - { - StringBuilder sb = new StringBuilder("ad"); - org.cprover.CProverString.insert(sb, 1, 'c'); - org.cprover.CProverString.insert(sb, 1, "b"); - String s = sb.toString(); - assert(!s.equals("abcd")); - } -} diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test.desc b/jbmc/regression/jbmc-strings/java_insert_string/test.desc deleted file mode 100644 index 698c2b13e345..000000000000 --- a/jbmc/regression/jbmc-strings/java_insert_string/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_insert_string.class ---refine-strings --string-max-length 1000 --function test_insert_string.main -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion\.1\].* line 8.* FAILURE$ --- diff --git a/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.class b/jbmc/regression/jbmc-strings/java_insert_string/test_insert_string.class deleted file mode 100644 index e5990e07a15d25e478bdb5a83afa107b1553147c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 897 zcmZuv*>2N76g`v8j^mKjNs|;PP$-b35VM3e6#~K{L|CLCQ2SCj_9(cxcCnrQ3;h9} z0VzRLf_MH2#2u$e1mR`o&bjBFyUhLh``dQ_P25(H!?J`EGEORp;gpOO1*dUFJXX`l z;;f8w3eKY{p{5`s$aMv4xFF#oLt)hj0`7;l=LQe#!00*LVqlvLsdd}6!#fP|YV9>c zqU~9nA=j~8{(P|0}#jcsGkP@$nfZei<=;r8`zGpmL0!X;E$!*KnPoGE=%YY4oA*dnBdJ*C64BikrB_ke|i9=xuW|{0kZv#jsfI z%y?t4C5E-+`F-8o^}Rjr>+P4(J&8$;yJmPiAAHzm>&bs)=b#ChrW|?`^2N76g`t|9M@^mbPIb6p(Jh7u#`2SEAT>Ekb*$;rE=nF<>J`E3ld+!dwzgt zij+!Jf_FX&xZ{wfX=VG4=gygP&s~21`SBCLGB#C=VMf8Mg6kYNRKzeNOy5|YkHyzu1W_o(V5(Wd?VMtU>+w@l$ zqJ`pHhS;WK2!?dcw8eJNY6$m@1k*uFH*JPg-PfBRw)A%BCT`NjagRZ%Hm(0mYTXIk zrg&k>d(*z~{9V1>7PhhLG!8`5Upmk~=^7?5NwkK!w?|9E3M5#blr7!fFV}t7wD&gx z(=vpsQ8Dgocz}l-k2E~S6OM|8DxPY{Vw|E&8p%OgG^}8iAvfS!@8|y9bsd)>dtMXA znuc|3Fk}YzUWIapTs>J-wq8aIr9$oOg-Y?1YbcKjDfOK`$3)>gkPxQ?)IWQ^Xi;yR zz-O53(V9;AHPyx^8lku7!gwfP*v-J(5@b=&CQnQ31+U0nC&b4R*arn|^=z++z#i++bXh}h3bGR6_n)@0^aX%oS9GGO8l5EOL`WQzE66TtyO1T~q{01u{YH(2aiY&)ZWg+BA* zqt9ZpC1Uj5KgdVoxt)xWm^SB}d(U^y{m$3h--q9S0+_)g4JnLpjB1GBf;1Ns7{etQ zUDj{~nFI`sb7VCnFd}y*;+T}_t8q+8pX0cu;X0-{ZZPzXnZ7T)z;Ydb!Sc;5TT~g? z21Bf1IaV;s5Y3FgU{H!~RWKx1Ek``5*S3WBT!JZ4GcAXqyA+s}H*4l@xXm#`BpKp` ziv6#RR&wiJMJ!pes3#D9@JeQ;cFcFCjsc_@3>oKa)7j3I0?%@`<^D}+ZgJe!aR+yG z+(VwDpyNJfb@ZX1Veq(Y{%Dv*&vQKqdcY77wvIW>GpNhLwp|?$QDjK8IdClKSj5r^ z22ZzkL?xi=O~R^~&7xF+lV4epQ76|AejsWjlv^kKz-maxa&ymUgn$MSW-U*8+QQim zUWa!(`wftN?slx6L0IL?bC6cfEMTcIDJ0N4@@ucUt03W z6QGu~At-sQT+ybBz>uyA-||GYEhK%`piT+81sfQp%ax*w$c#ZLJw;JaccjUlqSX+2 zMqbS}!M;i$2Fb?4O;Q}E+t5EysTlZVXg}1)*{HEx&MJl|XH~;4XJgWE!z~{mvQEvS zt6`w1O(<*oP$wFQHNf`~-$TD#7}{ra9U!sZg!Zci=pr}S067VoOz91D?{$L0+Eh;i z$&PKwIuf#;MUrBbo)|Q6TE%H(IfI5_bkVP+V;VguP^Lt}Y@in=$@8A1`AEn!RBa%7 zh!V$Hj&t;mrK!hITZ5TU7oay~G|;;Tu6%(K{f784i6iM`GZhhiP6|96ayS2z$O|#e9U^Nd3aKShdCefcB%mEjtS1TidFW8P-v_k66~F%D+v=#70Zu|@LS11M{-Y@jA|y+>~oa#&xDq*PsLXeU<~5~ zOLUCkXBh!g1bB`WLd}G1^hA8J@$OOVuGWbr1piXGcoE*OFyLUkD0g2fA12(5##(EJAb98+uS*C^T-DBr?4 zx`F%4a9BA<2%GOkF6i*$-)1QxBW2J%>MkaEGc+|Uu$dPHs-bs{(m7oF5_aJ`>=Eaq RF2hrV6}&a-r}L6Ce*kI)bz}el diff --git a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java b/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java deleted file mode 100644 index c052ed429bdf..000000000000 --- a/jbmc/regression/strings-smoke-tests/java_compare/test_compare.java +++ /dev/null @@ -1,9 +0,0 @@ -public class test_compare -{ - public static void main(/*String[] argv*/) - { - String s1 = "ab"; - String s2 = "aa"; - assert(s1.compareTo(s2) == 1); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test.desc b/jbmc/regression/strings-smoke-tests/java_concat/test.desc deleted file mode 100644 index 2672b7502d22..000000000000 --- a/jbmc/regression/strings-smoke-tests/java_concat/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -test_concat.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion.1\].* line 10.* SUCCESS$ -^\[.*assertion.2\].* line 11.* FAILURE$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class b/jbmc/regression/strings-smoke-tests/java_concat/test_concat.class deleted file mode 100644 index 8802b3957d256ad0dd0290b78212e49734f7f807..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 847 zcmZuvT~8B16g|`KSGNn4VzCtwL9A^B>PPj3#z?9pL_kc93A~u?c2XA0?q+t&kKsk% zd{&dzNTTolDD}=_TZ}x++_~r8x%Zqq^YhoY?*M9eWMUF?I<6a-H<7>%xh)vDDea<( zCEQBE!m^IrCQO-GG;s$d9c6}@WjhSHh+N+bpShvk>hd-NJ7Cc2uIENi7?P#(8wRD} zw>iVqw(IfT-f@eI*D{#`$F}P+Of)0gdADN+F-&Y2jJnhPTf=PnJ>l?8SKi1(JdEBt zzUSD{+L3)?TbM?caCxqFZLd>pM#A+v42i&%!HR{uSRpDw;9FS5nvSZ4d$@053K@p{ z_~yn?&T}Dr!H~YtOveKY4^jK4)yviqcOr&dX?tAdy#Klsu64QBi4NmAY>|7;o1u7F z{{JNy3cl!6oj~{}TvQu-u^sBuoI_h|Q1{tOs%@1UH1IL0Mwi}-QrkRq1#gd((&VEa z1?Zs;ut-lmN&kXn@^UtGN`lGx(mq4pJXuCotqj0E$wXYCU5i166mp}~4|G+f*sC)n z_OrMBH`> z2Ax&4k_J@3Kz_uw7ApXzvsNDyr_hy; YP?BGe8h0CtloeGZtfz7mg_z8>KR*en>i_@% diff --git a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java b/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java deleted file mode 100644 index 9e861e722bf7..000000000000 --- a/jbmc/regression/strings-smoke-tests/java_concat/test_concat.java +++ /dev/null @@ -1,13 +0,0 @@ -public class test_concat -{ - public static void main(/*String[] argv*/) - { - String s = new String("pi"); - int i = s.length(); - String t = new String("ppo"); - String u = s.concat(t); - char c = org.cprover.CProverString.charAt(u, i); - assert(c == 'p'); - assert(c == 'o'); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test.desc b/jbmc/regression/strings-smoke-tests/java_delete/test.desc deleted file mode 100644 index 7fb479f198b8..000000000000 --- a/jbmc/regression/strings-smoke-tests/java_delete/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_delete.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class b/jbmc/regression/strings-smoke-tests/java_delete/test_delete.class deleted file mode 100644 index 44a8fdc10db2d6d2f74b2300b796753d55a27517..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 856 zcmZWnZEw<06n<`@6iPQ3V~nX&r&EDB@CBy{ixHd+m<#_yM@36zg8wsYsq3L)GbM4TyKD;oGA~&hgaFZdqZMmm3dfV>_i$8N@Qa0p4 z_}=C&4|(;#JT?t1AjhyQ?V4+P-C8>oj@NzMb6lGXQqk;K611tIYM_Q&25#eyfef+? zO4Fip2JWKHP@Hl!$Gtrj!Y7jSKV>!CGq8pGBxaiMs&l}t@ITi`2g6dSHN}mb4LO(< zUvz8Mk?@bXsO`Lt-f>Q1)FH#xZ1QPmjosby4DmQd0}TB!S-vz2Y|x(g$DZj1X9SKK zX_RS^nW^j@m$uDNuzBDJZcoNTy9;|1pjGchVQB*GQmR6+>Isy+Tx^K=^GaO(2K8NKfJEyHv_A41x#R$;KGG-9 z_l8LSl$=V$S%6BmN>`g80U8QOVv{Nq$eRZHEw5o&Ly_DolcM!V2(XYd2AJzZi+@5q X_7&QccdS+Ns8EbYvZHfR+4Fw^Cq%Z1 diff --git a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java b/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java deleted file mode 100644 index 99298e536c36..000000000000 --- a/jbmc/regression/strings-smoke-tests/java_delete/test_delete.java +++ /dev/null @@ -1,10 +0,0 @@ -public class test_delete -{ - public static void main(/*String[] argv*/) - { - StringBuilder s = new StringBuilder("Abc"); - org.cprover.CProverString.delete(s,1,2); - String str = s.toString(); - assert(str.equals("Ac")); - } -} diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test.desc b/jbmc/regression/strings-smoke-tests/java_empty/test.desc deleted file mode 100644 index c1dae21b4d5b..000000000000 --- a/jbmc/regression/strings-smoke-tests/java_empty/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -test_empty.class ---refine-strings --verbosity 10 --string-max-length 1000 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class b/jbmc/regression/strings-smoke-tests/java_empty/test_empty.class deleted file mode 100644 index 8e9a17d387e018eab40fb786dd1c200c507739da..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 571 zcmY*V%T5A85Ugf_!F3fx#YM%piF%L=M`JX;4!#Z;6TO%PCT0{CvpbmhEBt_GHGxDE zz57kZ*t1cHm!5u9RaejF_v<@=5|(WYAeX|#00dkcc}xmS*+?KKFm0oN8G%{C=#m$P zGSI5&hr25DDs@>S&?OKL zd+gmsZGkyLYNJ~J)v(LWR#27u$}rMehWbi2?)1a@jd$-ka44(72yaLue( z_x$VP_MgYSAZP{zyRRUy=wQjx=4N)dMu(3^A^_Rn1ss?Mz~6WzTgUEIUDVXmLf@DBr7^d cwISkwOSRn%4)@GLSs~_Nh5wF7)|?PF3SyW-R{=ir9Xy0 z;Io>5v5CI>pES;03dHiVGdpwU%$b?{`|ppR0BU%kVICJ$tfp{LgMv#ME@Mr4SJKdN zHHCEz*Kl3M4Go$^mNishsMugwT<1X`{LuE?V8;%4+YucGw$G5Df+4_zViSB<7Zistyykb=<+Gjx2H{ zgV#1K>Z#){Y7C_*$>Z^WPkrAbmh73{D(>mn!hMF^wCGj)Kv>~_p^+GdrE+tM8wKlf zLo1%&HLWAxI~Km#cpcesO>#6U!`5u^>3H?s-O3E{I7gcdy)jv#JPWMT!NjK?cY-ql zM}yQWbkXcocEh2wGZZ@_uzk^)tcZ>n_9#I&-^Uugo_Ts=ELV~{CNBmiZ$#fk`dcN- z$R>;-*cS;zfxgKo$dJa;1p0wW70Q_>Q1z-Cc+U8a#5-evWb-T3J_;N8)Bx!| zGAGdXhRFPqq)J3uM1uSTz278}s#rz}RccYBXa?*LsuWXEqVUS3Yb{a&Eade8=K4_M ZpAnCJgF59Mi