From 3a13476d678027e0793e822e058fedcaa29da41a Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Tue, 25 Jul 2017 10:00:37 +0100
Subject: [PATCH 1/6] Fix formatting spotted by the linter

---
 .../get_numeric_value_from_character.cpp                        | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
index 29bef9bd788..d562cb1c5ac 100644
--- a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
+++ b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
@@ -25,7 +25,7 @@ SCENARIO("get_numeric_value_from_character",
 
   REQUIRE(from_integer(0, int_type)==simplify_expr(
     get_numeric_value_from_character(
-      from_integer('0', char_type), char_type, int_type),ns));
+      from_integer('0', char_type), char_type, int_type), ns));
   REQUIRE(from_integer(9, int_type)==simplify_expr(
     get_numeric_value_from_character(
       from_integer('9', char_type),

From ca96a491be1c3c7843c2e68ab3387167906429b5 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Wed, 26 Jul 2017 15:40:32 +0100
Subject: [PATCH 2/6] Refactor add_axioms_for_correct_number_format

# Conflicts:
#	src/solvers/refinement/string_constraint_generator_valueof.cpp
---
 .../refinement/string_constraint_generator.h  |  2 +-
 .../string_constraint_generator_valueof.cpp   | 38 +++++++++----------
 2 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index a969ad6594e..a4c5c543d1d 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -294,7 +294,7 @@ class string_constraint_generatort
     const function_application_exprt &f);
 
   exprt add_axioms_for_parse_int(const function_application_exprt &f);
-  exprt add_axioms_for_correct_number_format(
+  void add_axioms_for_correct_number_format(
     const string_exprt &str, const exprt &radix, std::size_t max_size);
   exprt add_axioms_for_to_char_array(const function_application_exprt &f);
   exprt add_axioms_for_compare_to(const function_application_exprt &f);
diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp
index 2995648dc38..3110c454607 100644
--- a/src/solvers/refinement/string_constraint_generator_valueof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp
@@ -364,12 +364,9 @@ string_exprt string_constraint_generatort::add_axioms_for_value_of(
 /// \param str: string expression
 /// \param radix: the radix
 /// \param max_size: maximum number of characters
-/// \return a boolean expression saying whether the string does represent a
-///   number with the given radix
-exprt string_constraint_generatort::add_axioms_for_correct_number_format(
+void string_constraint_generatort::add_axioms_for_correct_number_format(
   const string_exprt &str, const exprt &radix, std::size_t max_size)
 {
-  symbol_exprt correct=fresh_boolean("correct_number_format");
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
   const typet &char_type=ref_type.get_char_type();
   const typet &index_type=ref_type.get_index_type();
@@ -386,31 +383,34 @@ exprt string_constraint_generatort::add_axioms_for_correct_number_format(
   // TODO: we should have implications in the other direction for correct
   // correct => |str| > 0
   exprt non_empty=str.axiom_for_is_longer_than(from_integer(1, index_type));
-  axioms.push_back(implies_exprt(correct, non_empty));
+  axioms.push_back(non_empty);
 
   // correct => (str[0] = '+' or '-' || is_digit_with_radix(str[0], radix))
   or_exprt correct_first(
     or_exprt(starts_with_minus, starts_with_plus), starts_with_digit);
-  axioms.push_back(implies_exprt(correct, correct_first));
+  axioms.push_back(correct_first);
 
   // correct => str[0]='+' or '-' ==> |str| > 1
   implies_exprt contains_digit(
     or_exprt(starts_with_minus, starts_with_plus),
     str.axiom_for_is_longer_than(from_integer(2, index_type)));
-  axioms.push_back(implies_exprt(correct, contains_digit));
+  axioms.push_back(contains_digit);
 
   // correct => |str| < max_size
-  axioms.push_back(
-    implies_exprt(correct, str.axiom_for_is_shorter_than(max_size)));
-
-  // forall 1 <= qvar < |str| . correct => is_digit_with_radix(str[qvar], radix)
-  symbol_exprt qvar=fresh_univ_index("number_format", index_type);
-  exprt is_digit=is_digit_with_radix(str[qvar], radix);
-  string_constraintt all_digits(
-    qvar, from_integer(1, index_type), str.length(), correct, is_digit);
-  axioms.push_back(all_digits);
+  axioms.push_back(str.axiom_for_is_shorter_than(max_size));
 
-  return correct;
+  // forall 1 <= i < |str| . correct => is_digit_with_radix(str[i], radix)
+  // We unfold the above because we know that it will be used for all i up to
+  // str.length()
+  for(std::size_t index=1; index<max_size; ++index)
+  {
+    const exprt index_expr=from_integer(index, index_type);
+    /// index < length && correct => is_digit(str[index])
+    implies_exprt character_at_index_is_digit(
+      binary_relation_exprt(index_expr, ID_lt, str.length()),
+      is_digit_with_radix(str[index], radix));
+    axioms.push_back(character_at_index_is_digit);
+  }
 }
 
 /// add axioms corresponding to the Integer.parseInt java function
@@ -443,9 +443,7 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
 
   /// TODO: we should throw an exception when this does not hold:
   const std::size_t max_string_length=40;
-  const exprt &correct=add_axioms_for_correct_number_format(
-    str, radix, max_string_length);
-  axioms.push_back(correct);
+  add_axioms_for_correct_number_format(str, radix, max_string_length);
 
   /// TODO(OJones): size should depend on the radix
   /// TODO(OJones): we should deal with overflow properly

From 527c282288b4e364533a0fb2fc672618fa1c05fa Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Thu, 27 Jul 2017 10:20:23 +0100
Subject: [PATCH 3/6] Rewrite parseint code to use modulo

Should be faster (definitely when the radix is a power of 2) and cope with
a larger range of numbers. It doesn't have the old problems with detecting
overflow. Also update various tests, turning on ones that now run fast enough.
---
 .../java_parseint/test.desc                   |   7 -
 .../java_parseint/test_parseint.class         | Bin 914 -> 0 bytes
 .../java_parseint/test_parseint.java          |  12 --
 .../java_parseint_1/Test.class                | Bin 0 -> 1001 bytes
 .../java_parseint_1/Test.java                 |  19 ++
 .../java_parseint_1/test.desc                 |   9 +
 .../java_parseint_2/Test.class                | Bin 0 -> 737 bytes
 .../java_parseint_2/Test.java                 |  10 ++
 .../java_parseint_2/test.desc                 |   6 +
 .../java_parseint_knownbug/Test.class         | Bin 0 -> 825 bytes
 .../java_parseint_knownbug/Test.java          |  12 ++
 .../java_parseint_knownbug/test.desc          |   6 +-
 .../test_parseint.class                       | Bin 1089 -> 0 bytes
 .../java_parseint_knownbug/test_parseint.java |  21 ---
 .../java_parseint_with_radix/Test.class       | Bin 0 -> 1428 bytes
 ...est_parseint_with_radix.java => Test.java} |  14 +-
 .../java_parseint_with_radix/test.desc        |   4 +-
 .../test_parseint_with_radix.class            | Bin 1537 -> 0 bytes
 .../Test.class                                | Bin 0 -> 1035 bytes
 ...est_parseint_with_radix.java => Test.java} |   8 +-
 .../java_parseint_with_radix_knownbug/output  | 164 ++++++++++++++++++
 .../test.desc                                 |   4 +-
 .../test_parseint_with_radix.class            | Bin 1141 -> 0 bytes
 .../java_parselong_1/test_parselong.class     | Bin 923 -> 0 bytes
 .../java_parselong_2/test_parselong.class     | Bin 926 -> 0 bytes
 .../java_parselong_3/test_parselong.class     | Bin 927 -> 0 bytes
 .../java_parselong_4/test_parselong.class     | Bin 929 -> 0 bytes
 .../java_parselong_5/test_parselong.class     | Bin 949 -> 0 bytes
 .../java_parselong_binary_1/Test.class        | Bin 0 -> 854 bytes
 .../Test.java}                                |   4 +-
 .../test.desc                                 |   6 +-
 .../java_parselong_decimal_1/Test.class       | Bin 0 -> 828 bytes
 .../Test.java}                                |   4 +-
 .../test.desc                                 |   4 +-
 .../java_parselong_decimal_2/Test.class       | Bin 0 -> 832 bytes
 .../Test.java}                                |   4 +-
 .../test.desc                                 |   4 +-
 .../java_parselong_hex_1/Test.class           | Bin 0 -> 831 bytes
 .../Test.java}                                |   4 +-
 .../test.desc                                 |   6 +-
 .../java_parselong_octal_1/Test.class         | Bin 0 -> 834 bytes
 .../Test.java}                                |   4 +-
 .../test.desc                                 |   6 +-
 .../string_constraint_generator_valueof.cpp   | 147 +++++++++-------
 44 files changed, 341 insertions(+), 148 deletions(-)
 delete mode 100644 regression/strings-smoke-tests/java_parseint/test.desc
 delete mode 100644 regression/strings-smoke-tests/java_parseint/test_parseint.class
 delete mode 100644 regression/strings-smoke-tests/java_parseint/test_parseint.java
 create mode 100644 regression/strings-smoke-tests/java_parseint_1/Test.class
 create mode 100644 regression/strings-smoke-tests/java_parseint_1/Test.java
 create mode 100644 regression/strings-smoke-tests/java_parseint_1/test.desc
 create mode 100644 regression/strings-smoke-tests/java_parseint_2/Test.class
 create mode 100644 regression/strings-smoke-tests/java_parseint_2/Test.java
 create mode 100644 regression/strings-smoke-tests/java_parseint_2/test.desc
 create mode 100644 regression/strings-smoke-tests/java_parseint_knownbug/Test.class
 create mode 100644 regression/strings-smoke-tests/java_parseint_knownbug/Test.java
 delete mode 100644 regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.class
 delete mode 100644 regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java
 create mode 100644 regression/strings-smoke-tests/java_parseint_with_radix/Test.class
 rename regression/strings-smoke-tests/java_parseint_with_radix/{test_parseint_with_radix.java => Test.java} (77%)
 delete mode 100644 regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.class
 create mode 100644 regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.class
 rename regression/strings-smoke-tests/java_parseint_with_radix_knownbug/{test_parseint_with_radix.java => Test.java} (78%)
 create mode 100644 regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output
 delete mode 100644 regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.class
 delete mode 100644 regression/strings-smoke-tests/java_parselong_1/test_parselong.class
 delete mode 100644 regression/strings-smoke-tests/java_parselong_2/test_parselong.class
 delete mode 100644 regression/strings-smoke-tests/java_parselong_3/test_parselong.class
 delete mode 100644 regression/strings-smoke-tests/java_parselong_4/test_parselong.class
 delete mode 100644 regression/strings-smoke-tests/java_parselong_5/test_parselong.class
 create mode 100644 regression/strings-smoke-tests/java_parselong_binary_1/Test.class
 rename regression/strings-smoke-tests/{java_parselong_5/test_parselong.java => java_parselong_binary_1/Test.java} (76%)
 rename regression/strings-smoke-tests/{java_parselong_3 => java_parselong_binary_1}/test.desc (66%)
 create mode 100644 regression/strings-smoke-tests/java_parselong_decimal_1/Test.class
 rename regression/strings-smoke-tests/{java_parselong_1/test_parselong.java => java_parselong_decimal_1/Test.java} (74%)
 rename regression/strings-smoke-tests/{java_parselong_1 => java_parselong_decimal_1}/test.desc (70%)
 create mode 100644 regression/strings-smoke-tests/java_parselong_decimal_2/Test.class
 rename regression/strings-smoke-tests/{java_parselong_3/test_parselong.java => java_parselong_decimal_2/Test.java} (75%)
 rename regression/strings-smoke-tests/{java_parselong_5 => java_parselong_decimal_2}/test.desc (70%)
 create mode 100644 regression/strings-smoke-tests/java_parselong_hex_1/Test.class
 rename regression/strings-smoke-tests/{java_parselong_2/test_parselong.java => java_parselong_hex_1/Test.java} (73%)
 rename regression/strings-smoke-tests/{java_parselong_4 => java_parselong_hex_1}/test.desc (66%)
 create mode 100644 regression/strings-smoke-tests/java_parselong_octal_1/Test.class
 rename regression/strings-smoke-tests/{java_parselong_4/test_parselong.java => java_parselong_octal_1/Test.java} (74%)
 rename regression/strings-smoke-tests/{java_parselong_2 => java_parselong_octal_1}/test.desc (66%)

diff --git a/regression/strings-smoke-tests/java_parseint/test.desc b/regression/strings-smoke-tests/java_parseint/test.desc
deleted file mode 100644
index 3b38dc2c575..00000000000
--- a/regression/strings-smoke-tests/java_parseint/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE
-test_parseint.class
---refine-strings
-^EXIT=10$
-^SIGNAL=0$
-^\[.*assertion.1\].* line 8.* SUCCESS$
-^\[.*assertion.2\].* line 9.* FAILURE$
diff --git a/regression/strings-smoke-tests/java_parseint/test_parseint.class b/regression/strings-smoke-tests/java_parseint/test_parseint.class
deleted file mode 100644
index 0f021d000fa3d68a1caa7d62f1a9090f569d5d01..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 914
zcmZ`%%Wl&^6g^`*w&S?uMM@|IS}2gDv>^~S^dV3IsZxMNP^Fdynk1tz#dRv%DgV+9
z6&u!oL=ctAo<Cv%;*KeaLd(K)=f2K8_jtbl`g#PQj=K(0xMJa|jX4Jzt~t1l8%ZQl
zvQTzlsbs~$JZ@T8V93w$Fcd)~dw%#(hP>s84g=d_Fqfq-qg4jIRNi1P)_NVmkZwp{
zJniqaMDSb{Gvpe*HupAoAeDa{G@@5BRMn9PqnEop2!-^cC4$-E(r1_~y=ZLnJzn*=
z->o*IK>FP!HO7qI2yZWjJ&|XyVx&%u7_Ji*54toYe+m@CL^I;;*H8Fv%!mYGu$SB3
z@lH;&*ALp_v5YquBe|&Nx;TS0L*`!&3|j5BN-kQcy10d!3l|d%#Zl#hzk)srf?hyO
z#^5bb{~grFz@N3YMLS|BlulPAJ3?RgBheKEYsXrU`=2%vC_QRh^XNa5?i~@zKy-#2
zNu{Vy3Hr%fn5AcuqG!Z1MYR>(bTFj^of-0~WEt5+WdQbpE*i3QnsJa`0^Qv|1<2zp
zc}Wy7NfFijj=*%XtCb_;0QU}|ZRYd=jK=&IBvwAc+(&jg<Gw}e5Z2}Z_P1f|U=&kR
z^?2$O%_S;ynuKrBBpYR#xI!x^CNor*!2-^qNDK-n;XI~@F)_deOq0Dxp9}3L$`&rM
qAH><l<>9jRcoQI-OMZs456gHDL;nQx<l+h_0nNRy<e4Ey!|ZR-LA-VV

diff --git a/regression/strings-smoke-tests/java_parseint/test_parseint.java b/regression/strings-smoke-tests/java_parseint/test_parseint.java
deleted file mode 100644
index d9b84914c7c..00000000000
--- a/regression/strings-smoke-tests/java_parseint/test_parseint.java
+++ /dev/null
@@ -1,12 +0,0 @@
-public class test_parseint
-{
-    public static void main(String[] args)
-    {
-        if (args.length == 1) {
-            String twelve = new String("12");
-            int parsed1 = Integer.parseInt(twelve);
-            assert(parsed1 == 12);
-            assert(parsed1 != 12);
-        }
-    }
-}
diff --git a/regression/strings-smoke-tests/java_parseint_1/Test.class b/regression/strings-smoke-tests/java_parseint_1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..81304601f473385534b4e8453a7e7cf7a28b7d53
GIT binary patch
literal 1001
zcmZ`%-A~g{96h())~yux!Ka8HD98X|GA5vcXh0K^i4P+r@M6k#oyF0TwnGz5{6Bb+
zH=fl*j3oN*f8+z=X`P!w%(C|W&b{aNJLlYf|M}%BfC6soXvdI->v0V0P>|Izg3$!p
zFs9*#4h=(bjH_=?PEIsT=*Z!whDm{rLDTc3>syZPEm@wqS(6n3u^|wfvuw-1C!l6W
z)&wGpPDKhNi<T`{>f4*rT@4NkWQtDNtgV@@71Rwd;y<@M_9(7O&%eta&m4z6vdclM
znEz7Nc0=lxxohTXrd`dIeAlw8JgV)Ot|u$hCYD)ko3EZ)w%^3_#4UmLl5dt@JT`a2
zf%Gj9pDWiIlJ$~PcgymT6$nfO8YY5C22w~1q)ty2P$u)iW?sXT!8C6fIESP_Z|mfP
zKQTRYUB?yB^OJ>{!tB&^VTQ(n5gMiq%wYDP0Z%r!WSQ!_vc*=fhSwmAbPHX!eOZ-k
z9S;*=`5zi%Nw#Q<HQt~=cSU-ZD=ST%49Kr@gV(o#0e%SW{7^)yH*m(43hG3f&kU;^
z--7Sx=pn>=E);a|84E#yPOgpL2hfFXRtfZ=mk7zChs{)CZ~7wpm_LHDo>31GDUN+c
zbp8Wkdr0@EjCW`|g0_B$__rpu-@*>C&==juosgb5P0#3O=^6bmdZ1YiHRq|6M)-@-
zs7CE^WT|%!Iu;ni5`$P_2qo@T8Nq9M2>cbuNMao4(MMmM<Xk{Mb66pEF~my5E`=Dq
z;xbpj75;k=Jw{f;fcSw9<ru?_B?n(^CR_;P1JaqcPcZhNMGg>AKO%NE?Vx8Aig7=<
KlWQy#4E_SLX2Hz>

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parseint_1/Test.java b/regression/strings-smoke-tests/java_parseint_1/Test.java
new file mode 100644
index 00000000000..8831b817489
--- /dev/null
+++ b/regression/strings-smoke-tests/java_parseint_1/Test.java
@@ -0,0 +1,19 @@
+public class Test
+{
+    public static void foo(int i)
+    {
+        if (i == 1) {
+            String twelve = new String("12");
+            int parsed1 = Integer.parseInt(twelve);
+            assert(parsed1 == 12);
+            assert(parsed1 != 12);
+        }
+        else if (i == 2) {
+            // 2^31-1, max value of Integer
+            String max_int = new String("2147483647");
+            int parsed2 = Integer.parseInt(max_int);
+            assert(parsed2 == 2147483647);
+            assert(parsed2 != 2147483647);
+        }
+    }
+}
diff --git a/regression/strings-smoke-tests/java_parseint_1/test.desc b/regression/strings-smoke-tests/java_parseint_1/test.desc
new file mode 100644
index 00000000000..b0e5d799277
--- /dev/null
+++ b/regression/strings-smoke-tests/java_parseint_1/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.foo --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+^\[.*assertion.3\].* line 15.* SUCCESS$
+^\[.*assertion.4\].* line 16.* FAILURE$
diff --git a/regression/strings-smoke-tests/java_parseint_2/Test.class b/regression/strings-smoke-tests/java_parseint_2/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..58992e04a96ae1b0ad55f5e611fa582ee161e434
GIT binary patch
literal 737
zcmZuvO>fgc5PfSq*~E3JlhP29@=+*|1c?Z#w?+t5K#COLkg5{BppCtREyj-48-7er
z+&BXgMIgbQ--HmeCNzg~nJ>S2^JdmRe}DZBU<bE-RIuse5-wL!#ubjMK0Iu4Z27o`
z>m1t*>)RsFr8X){^M@)IlSIZ0?2w^6P^mKa7~D?xfWh0#V#%;JQmK48e>0JK-+~$H
zqbw51fzZn4i=t;<shl`Q`!YAX#PKrA7&bbiBk@-B6Om5)W203%-L>3-N@sKPA}=bI
z@eGQA&xFope3!%x8CJ(eM6aKS*<xO05G4z_{y3ZKNIq6pT-DCMW9b5{AmF$W;3jSb
zsKRGxF6TV>cZEk<XPVZvjU1f-UGx~jCGy$iNJfUCwk!=(Bd3zODuqZ&85;lDb=W28
zYs<d9gpN<pSmsL0_*4TeXXf;QE`NwEdb<ieC<~ibHAOC%U54x`WqtCDe5rQ=_JINi
z=g5|eB8{WiLJ5EnHS$%|u}&4+JSDV4zTFGMFK`C!(mT{X!ac^yH+auaQ2Jph-GZ`C
ze~+c%L>`cB5tXHH{H4HoY*5C@H*kRlG$|t)ztEz~;Nq#`ok9*!tCv56AA@`E;klpS
To>gxtN^pYvcE=Va4%&YJT_%n~

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parseint_2/Test.java b/regression/strings-smoke-tests/java_parseint_2/Test.java
new file mode 100644
index 00000000000..a32036c75ab
--- /dev/null
+++ b/regression/strings-smoke-tests/java_parseint_2/Test.java
@@ -0,0 +1,10 @@
+public class Test
+{
+    public static void foo(String input_string)
+    {
+        int parsed1 = Integer.parseInt(input_string);
+        if (parsed1 == 2) {
+            assert(false);
+        }
+    }
+}
diff --git a/regression/strings-smoke-tests/java_parseint_2/test.desc b/regression/strings-smoke-tests/java_parseint_2/test.desc
new file mode 100644
index 00000000000..60c72ba9b36
--- /dev/null
+++ b/regression/strings-smoke-tests/java_parseint_2/test.desc
@@ -0,0 +1,6 @@
+THOROUGH
+Test.class
+--function Test.foo --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* FAILURE$
diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/Test.class b/regression/strings-smoke-tests/java_parseint_knownbug/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..dd9c488696240aebb743fb50bf4c19a59a8212be
GIT binary patch
literal 825
zcmZ`%O>fgc5PfSWS;uin;?fW(UnK?7KpWavG!hX46_6@Idq`EOy&xxE!j{yoY=<*H
zfM3uH+&BXgK~#b}{|UsbDT$!svO6<7^X9#o{r>aIR{#zgCM;a$m@{z2gocWVd0frH
z#5MgDWpG?KVW^C%i3QX+ZZJ&GyHO;<SO$LdKt^tNAUp=P%aCbFU&ePC^y<PkLuxJX
z1Vg?peX%jz?}~6sB{SIVpyv*@-B2q3IGBo`%ZM=ATOx|@5XQ40VBq`Ge=7Z0745k%
z-TJ`w`}Iy7O21D@{J;$(;WeoLI>S^ac6%?LxCaR&$zm{Cy}>alvl9%%o_Hh`g{<nb
zq!2CSQD7+ii_VZ+Tv>Kjoo3^<(^OeEITkG}p>AOcrx?nUlKX!q@-Pg8kfbYkj$0O%
zvGN!AW_M5YNX|_4q#iZ2;skWvk40Y)nvtj^_djJMJwGX18_<3jN}h;hD7-N>8csZ<
z2U^Z9=4i(jZI~6xN(@;#2n7W?i{#bmW^|`(Be3^mXt3$bBtiNEWLv)za2hk@Wl<Uz
zza}t^V$CCHJGMST>T&He(yb539HKaD^Eb#H!Pprg`)wS1JBg`&deX0iG})ZU8bmIO
z3R$bjCH+g(!=!bbL78&$^gqwy9C4Z@k3RDcR5;GFX{x+1X67WEfue1GLhcYe^$sch
VBQhr?Dws4h>z*3KMRGJ;`UQBzp3(pS

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/Test.java b/regression/strings-smoke-tests/java_parseint_knownbug/Test.java
new file mode 100644
index 00000000000..bb63540ad96
--- /dev/null
+++ b/regression/strings-smoke-tests/java_parseint_knownbug/Test.java
@@ -0,0 +1,12 @@
+public class Test
+{
+    public static void foo()
+    {
+        // -2^31, min value of Integer, and longest string we could have without
+        // leading zeroes
+        String min_int = new String("-2147483648");
+        int parsed3 = Integer.parseInt(min_int);
+        assert(parsed3 == -2147483648);
+        assert(parsed3 != -2147483648);
+    }
+}
diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
index f543e2d900b..c8084216052 100644
--- a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
@@ -1,12 +1,10 @@
 KNOWNBUG
-test_parseint.class
---refine-strings
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 10.* FAILURE$
-^\[.*assertion.3\].* line 17.* SUCCESS$
-^\[.*assertion.4\].* line 18.* FAILURE$
 --
 --
 Issue #664 is about turning these tests on
diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.class b/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.class
deleted file mode 100644
index 59932ae0cd7421d1da7759308ce69496d0710978..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1089
zcmZ`%OHUI~7(KVscBaz-`jD6J2TEInN*Mup7z|26Qk4WD0T*OwCv~t)$;@Ef`1l=c
zWXD=f#7KgB|B(yCGed2~;$rUH@7(Wv-}%nHKYo2X1fXM5MLYUsWE5mogpgA)fZH)>
z7?j=}A0NvYQlX$<L0)=KhKxHZhEb3)B9QJgT-S6wt7f|oE!SADnq>j8DiEErY|FbZ
zAZ4=40^!+O*%as~TDJLQdvo1%p83fFsbZ~URF@6M^5Z%f_Fh=7pY55hx3*<Cu4&oc
zB+G0XmMzegd0yNwUK#nSVOR2to@3dSNxzM}X}n%zs$aJyfyY6qa)A=({bb8NNv`7@
zC~P<tc21vBU!ZN#GfFQX8(V=)S|*@Om8$hY)y3MjQ!?kQV60QhhkPv>l1K?8{?#R*
z7KZgPeSBn8AM=xR8Fw{|f<Xro0zFN}gFkLRa-5nY5Fcz%$EojBQyJqL?qT9o%ctub
zW{LK6W?KF64NNwB&D)+?G1){3Tx0kj8m;VT(q^lC61<|a=~|9iZYZXA-Zl^T9#(OU
z&#Rq}NhEsw8M%|d=16f(Gs^QX_>biFAwF^w!a1(d0Hh4=wUY#Np_@?*J?JGuvgl<o
ziP+oRVPqH62MDdCq<w^o178uD{)Ffbk{46*2gDDctn4H9y@BmEu|3S>4x_u62>5CX
zKYj*3{ukd@Ed{Cz)XGt)UgoF@)yI&9ifP0#!?QVBu)vcg8eq|aH)Qz}>f|Iai1WC>
z$vTn2MO>m23&bu5*b=cT0mf-@m9_%c`E?_5gshAk;wRFfBV_7ZHt%bAtOo`H$&~g5
dZ99;|dk9OP5pDI`uNgr|oAGbuCW8=e{RT?A;tK!(

diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java b/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java
deleted file mode 100644
index d2283bbfccd..00000000000
--- a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java
+++ /dev/null
@@ -1,21 +0,0 @@
-public class test_parseint
-{
-    public static void main(String[] args)
-    {
-        if (args.length == 2) {
-            // 2^31-1, max value of Integer
-            String max_int = new String("2147483647");
-            int parsed2 = Integer.parseInt(max_int);
-            assert(parsed2 == 2147483647);
-            assert(parsed2 != 2147483647);
-        }
-        else if (args.length == 3) {
-            // -2^31, min value of Integer, and longest string we could have without
-            // leading zeroes
-            String min_int = new String("-2147483648");
-            int parsed3 = Integer.parseInt(min_int);
-            assert(parsed3 == -2147483648);
-            assert(parsed3 != -2147483648);
-        }
-    }
-}
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/Test.class b/regression/strings-smoke-tests/java_parseint_with_radix/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..26bc43a8c10a59cf847a0d5c0ce4782097700684
GIT binary patch
literal 1428
zcmZuwOHUI~7(I9Tm|-aNfgltV@mWwPMGzlA#Ucp_J`xNBc0)VjKyAs);6fKBYU0|R
zaU(kxx=|A`lBkI;j7wMk2>*aF8qXc*18kbi{qDKncfQB@`t9%g4*&)+p(Bi56@40#
zIu!KlNMWE34LGf0P=|_M4MQ5vXc*RTR>e6T=W#*Bh(Oa(!*NX8wTcC2!g7qoyqOaa
z3j)Crt6;ff0=`7|tbjjL%$Wk=X{%sfUAw(#+Bc-LKy130HS)8DZOQu%=yz{f4mqZ8
zn2vja95;(aawMiaD#x``GH}_rV<huNVJSJ|+E!tSj_RsmJ7$j0Vu}Iu94LddByhS6
z(2~Gl8K5PBp)x>ASON_*u9022Vyt@QaZ&=>NH)LIpgvPvv$N);CEKZ!75B-?LWrSB
zAhNegQclXZQ59n$q;WBX2%-Y5702<?OfTDZ(PsOp0oJMv53|1BR6o1(_xBr@c*txj
z#zVM-%&uJ57MIPeE6|+ye@t?S(Mq<df@?0BOrv?j<5i%gM%Yw0M;flgW%AUXt~t}O
zY%^Cbn!|F}_(0(o(8V<hbInAgRklgX2Wp2Ve)sW~<SBRtdNv_m(NNILZ_ootPCK;i
zfc<FYtqyI76JfCOh-5x;PsIJ}NN+)zkNGy?pFSChyhC90HG<C&?TCb*qkaqO{3f)I
zWo*5IZHPcTP$H<?CeW)1?$sc;S51H~@nDHS-zLzi3DPwP(z^&A#?^I<c`ej?1cB=K
z-!<ZY?~2dFwNiX&?+9WYQM}m8;DJ>Xa`rxN_IGiRc7VSirBkVah91s+3_8Y9k4Y+W
zowClM5i9h#PhlTW+Q*dj359)1ZC;Y;6C*!UwXf9eJ5~EZ-F~8-YIg`94hRhgMGT#y
z4TnS@x<m#?JiS+$Bh1BUM+bFoK>`O@k;0rwbb8nvu|ppAgjkn{JtcP7!@i@BOfvQd
zv7-`Wo)nHrjM;i{-1Fn!-~=tu3pk6$Kj=}>Eq<X%`GfA7W}<@b`0n$jQ(EUiZ&!h6
htl=#hpF#C+!0&s5;Qy;FlLnxKF3LZ^NnRA3`Ui@k7C!(0

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.java b/regression/strings-smoke-tests/java_parseint_with_radix/Test.java
similarity index 77%
rename from regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.java
rename to regression/strings-smoke-tests/java_parseint_with_radix/Test.java
index 978bf9fb320..29716aa2486 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.java
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/Test.java
@@ -1,32 +1,32 @@
-public class test_parseint_with_radix
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo(int i)
     {
-        if (args.length == 1) {
+        if (i == 1) {
             String str1 = new String("F");
             int parsed1 = Integer.parseInt(str1, 16);
             assert(parsed1 == 15);
             assert(parsed1 != 15);
         }
-        else if (args.length == 2) {
+        else if (i == 2) {
             String str2 = new String("123");
             int parsed2 = Integer.parseInt(str2, 10);
             assert(parsed2 == 123);
             assert(parsed2 != 123);
         }
-        else if (args.length == 3) {
+        else if (i == 3) {
             String str3 = new String("77");
             int parsed3 = Integer.parseInt(str3, 8);
             assert(parsed3 == 63);
             assert(parsed3 != 63);
         }
-        else if (args.length == 4) {
+        else if (i == 4) {
             String str4 = new String("-101");
             int parsed4 = Integer.parseInt(str4, 2);
             assert(parsed4 == -5);
             assert(parsed4 != -5);
         }
-        else if (args.length == 5) {
+        else if (i == 5) {
             String str5 = new String("00aB");
             int parsed5 = Integer.parseInt(str5, 16);
             assert(parsed5 == 171);
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test.desc
index e6138767e20..8b4a846fa3b 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test.desc
@@ -1,6 +1,6 @@
 CORE
-test_parseint_with_radix.class
---refine-strings
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.class b/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.class
deleted file mode 100644
index 22a393e7d103823ba68cca1ced4d362e5178623f..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1537
zcmZ`&&rcL*7=FIl*_~ln*k4+x0!p<l43%X8#TH~0&`7dvlhT-A4`kS#;MirC%nWU#
zClh;U&z|&9ZXP_C)<ldZ+d~sgnw~xRM|d^H#^?KBe*o)YX5R1l-uHQbJn#Jb|I-?P
zNnEs$z^H+&i7^Wrau&uh(Sa^Z8aQpiz^I8cCZ<fBHSwi^uPjVs#=tp&%t<E*TtD=x
zm0-aOoYk^h5)fAfVl!UF3ugr)L&H}D^!aMZ6-X4kiu=vx`l{=HFP#O_g=*0$UvYd-
zo_9e#yygW0M+%`Egex14AGls6T>04xudVn_$@^uRjO&h95%_56hr)H|CnsBWDr?!L
z(Dy29(<);S`Z>ve;8ws;lqFt^MKaNIyaCdZz(fO}C4tEXKuZFr8vrfc@z+>!rcE&d
zT}z=;{PAmNL$$|A3z##-^6r4FrRt_%bT4^w9Q_~acvQ9#M;aM{<o=e}$0d0;Yak!T
zd0dDiiIhNZ)A2%Gr;EN{^(jkkoQ-KyQ>^_|Zj7VQ$HtsF#(by(19NfAV_{GJZ&$Co
z#Zchz(7`!N6;jO#7Av8<<}$UZrq82P?_k*CFf~au<L1lUF}jxA!1LWwqY(}@+~frp
z>?#Jit_iNQNcPIsX+=Qsk>UFgPg#BizfpS|;!heH4)YyTAjxURcO1}zUY<JeF^&*n
zu=X3tBII7QYx)-Q&!8=*BiqmmBgy0wM9=+&*j=Rhl8Hai`3%PLHq5^p*j5v}FFNd6
zw9e46!(g>C+-$>evy}la>{_hOVC^uNtql1#4Ea3_zuGlp3$v<=PQ?&yC3xG0;O!oQ
z1-oX}3F7<5knT(2!F~z_ws1%RB1(W87@!@c5HadzaQG%hIQ%>;%%KyPDa&`%b{XAR
zr^2`Bb({MBPHpc{-Fp=1A({T6gwGlMAH{n~>0VL1*ElM4^a%s~q6-6}2gk$!j*AHl
zipw~mMBiYJB)8)z`Y3h}hS1N7H0I3Wn8KEc9aq>LVuK31N9+@Yy~HS)Wb7+qCnd%_
zIeaQHX0!2`^5gR0b9w;7e9of#9Yze;;tev|JJ@Z_;U>E4dq_>EzSEOxVS!Y->oL0T
c!qD$Sk32%`;C{=bQE2h=@-O&;2Mwp*10GLAApigX

diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.class b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..507c0f9f16b5fadb2004d17ab72f384c4f076501
GIT binary patch
literal 1035
zcmah|-%ry}7(I90)~+k;2Z}iH7a|T21~^3p`4N<4$y5@^5_l`y6^nBvZShh3J9v>d
zp4CK*B>L`u<OAZlWik{J+ob*Ox!?J|@0{EI`1SQ0fFd56Xh)xpTL$tbBIq|UfWZVT
z+}5@Z4-a(=nK002U|4%chK_=X5sc~>6X@u*eP4Qk<2L-qj&HBlWlcb=2*f9yh7(K)
zX!-t%Ky=QnNr6<^X~<`ruUDnFq>=@)Ww&bAE4JsTbrXyRFCCvX%1hD@CRpQz>#|0^
z6qfP>Z&VT2?KgIzZa3Bni-G4f)|jYo*q$$I+!iGgn8_iVAS2-jv@Hg9_0>~*BkV=p
z0>)&u-kjE4bT_@KoOjf03DtgBwXu*vRv`UvOLE8Ok1myRM@P}ZUEH&fLRz4!l|TE(
zrzf80dICK|qa**hC_oLMW8A`hJou~q^VM}(4Ft~TPurkO%CtI{8i8DsY-xn%a4FDv
z2CdXj%Tg`gT%Bjj)SC1iPu7kF(7#}l8$8$*T<3Sv&aXnGyOd-`8rU6KK0CN7@Gba`
z4eUXDU=YDMKI0+C@fll33FyQHt`g|NMIt1N9E)khwsO%OOz$JIoYnRaEf1#CUl4or
z5%Fzgy0iLwB==z~?;-L17~5%KyO_zvb}$hZFv9||ll<fv{NxF~8e0p;9^<go!ds_W
zgCi&SvzVAd60_W!rxy#{snCgay6~1Vl*A$#DSDB^B}(f=9^JT1D;6+}D<M`Pb~VH(
z7uOhp-h!6I4ltmjNBl%b<N*0*$mTbWO)iEG0-3D!8ExCpqq~S|pAbK7xT+aL#F|mZ
K(#u5zH-7_Q@W%K6

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.java b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.java
similarity index 78%
rename from regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.java
rename to regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.java
index 7279127d053..e7cbf6df57b 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.java
+++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.java
@@ -1,15 +1,15 @@
-public class test_parseint_with_radix
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo(int i)
     {
-        if (args.length == 1) {
+        if (i == 1) {
             // 2^31-1, max value of Integer
             String str1 = new String("7FFFFFFF");
             int parsed1 = Integer.parseInt(str1, 16);
             assert(parsed1 == 2147483647);
             assert(parsed1 != 2147483647);
         }
-        else if (args.length == 2) {
+        else if (i == 2) {
             // -2^31, min value of Integer, and longest string we could have
             String str2 = new String("-100000000000000000000000000000000");
             int parsed2 = Integer.parseInt(str2, 2);
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output
new file mode 100644
index 00000000000..e9cde4a8842
--- /dev/null
+++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output
@@ -0,0 +1,164 @@
+CBMC version 5.7 64-bit x86_64 linux
+Parsing test_parseint_with_radix.class
+Java main class: test_parseint_with_radix
+Converting
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Partial Inlining
+Generic Property Instrumentation
+Starting Bounded Model Checking
+Unwinding loop __CPROVER__start.0 iteration 1  thread 0
+Unwinding loop __CPROVER__start.0 iteration 2  thread 0
+Unwinding loop __CPROVER__start.0 iteration 3  thread 0
+Unwinding loop __CPROVER__start.0 iteration 4  thread 0
+Unwinding loop __CPROVER__start.0 iteration 5  thread 0
+Unwinding recursion java::test_parseint_with_radix::clinit_wrapper iteration 1
+Unwinding recursion java::test_parseint_with_radix::clinit_wrapper iteration 1
+size of program expression: 530 steps
+simple slicing removed 50 assignments
+Generated 68 VCC(s), 9 remaining after simplification
+Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier
+converting SSA
+Running string refinement loop with MiniSAT 2.2.1 without simplifier
+BV-Refinement: post-processing
+BV-Refinement: iteration 1
+54337 variables, 39117 clauses
+SAT checker inconsistent: instance is UNSATISFIABLE
+BV-Refinement: got UNSAT, and the proof passes => UNSAT
+Total iterations: 1
+BV-Refinement: post-processing
+BV-Refinement: iteration 1
+54337 variables, 39117 clauses
+SAT checker inconsistent: instance is UNSATISFIABLE
+BV-Refinement: got UNSAT, and the proof passes => UNSAT
+Total iterations: 1
+Runtime decision procedure: 0.386s
+
+** Results:
+[pointer_dereference.1] reference is null in *stub_ignored_arg1: SUCCESS
+[pointer_dereference.2] reference is null in *stub_ignored_arg1->data: SUCCESS
+[pointer_dereference.3] reference is null in *cprover_string_array$7: SUCCESS
+[pointer_dereference.4] reference is null in *this: SUCCESS
+[pointer_dereference.5] reference is null in *stub_ignored_arg0: SUCCESS
+[pointer_dereference.6] reference is null in *stub_ignored_arg0->data: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.1] reference is null in *args: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.2] reference is null in *new_tmp0: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.3] reference is null in *new_tmp2: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.1] assertion at file test_parseint_with_radix.java line 9 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 20: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.1] Throw null: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.4] reference is null in *new_tmp3: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.2] assertion at file test_parseint_with_radix.java line 10 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 29: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.2] Throw null: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.5] reference is null in *args: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.6] reference is null in *new_tmp4: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.7] reference is null in *new_tmp6: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.3] assertion at file test_parseint_with_radix.java line 16 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 52: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.3] Throw null: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.8] reference is null in *new_tmp7: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.4] assertion at file test_parseint_with_radix.java line 17 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 61: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.4] Throw null: SUCCESS
+[pointer_dereference.7] reference is null in *this: SUCCESS
+[array-create-negative-size.1] Array size should be >= 0: SUCCESS
+[pointer_dereference.8] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.9] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.10] reference is null in *this: SUCCESS
+[pointer_dereference.11] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.12] reference is null in *this: SUCCESS
+[pointer_dereference.13] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.14] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.15] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.16] reference is null in *this: SUCCESS
+[array-create-negative-size.2] Array size should be >= 0: SUCCESS
+[pointer_dereference.17] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.18] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.19] reference is null in *this: SUCCESS
+[pointer_dereference.20] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.21] reference is null in *this: SUCCESS
+[pointer_dereference.22] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.23] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.24] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.25] reference is null in *this: SUCCESS
+[array-create-negative-size.3] Array size should be >= 0: SUCCESS
+[pointer_dereference.26] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.27] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.28] reference is null in *this: SUCCESS
+[pointer_dereference.29] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.30] reference is null in *this: SUCCESS
+[pointer_dereference.31] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.32] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.33] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.34] reference is null in *this: SUCCESS
+[array-create-negative-size.4] Array size should be >= 0: SUCCESS
+[pointer_dereference.35] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.36] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.37] reference is null in *this: SUCCESS
+[pointer_dereference.38] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.39] reference is null in *this: SUCCESS
+[pointer_dereference.40] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.41] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.42] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.43] reference is null in *this: SUCCESS
+[array-create-negative-size.5] Array size should be >= 0: SUCCESS
+[pointer_dereference.44] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.45] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.46] reference is null in *this: SUCCESS
+[pointer_dereference.47] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.48] reference is null in *this: SUCCESS
+[pointer_dereference.49] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.50] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.51] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.52] reference is null in *this: SUCCESS
+[array-create-negative-size.6] Array size should be >= 0: SUCCESS
+[pointer_dereference.53] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.54] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.55] reference is null in *this: SUCCESS
+[pointer_dereference.56] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.57] reference is null in *this: SUCCESS
+[pointer_dereference.58] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.59] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.60] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.61] reference is null in *this: SUCCESS
+[array-create-negative-size.7] Array size should be >= 0: SUCCESS
+[pointer_dereference.62] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.63] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.64] reference is null in *this: SUCCESS
+[pointer_dereference.65] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.66] reference is null in *this: SUCCESS
+[pointer_dereference.67] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.68] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.69] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.70] reference is null in *this: SUCCESS
+[array-create-negative-size.8] Array size should be >= 0: SUCCESS
+[pointer_dereference.71] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.72] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.73] reference is null in *this: SUCCESS
+[pointer_dereference.74] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.75] reference is null in *this: SUCCESS
+[pointer_dereference.76] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.77] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.78] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.79] reference is null in *this: SUCCESS
+[array-create-negative-size.9] Array size should be >= 0: SUCCESS
+[pointer_dereference.80] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.81] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.82] reference is null in *this: SUCCESS
+[pointer_dereference.83] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.84] reference is null in *this: SUCCESS
+[pointer_dereference.85] reference is null in *cloned_array: SUCCESS
+[pointer_dereference.86] reference is null in cloned_array->data[index]: SUCCESS
+[pointer_dereference.87] reference is null in this->data[index]: SUCCESS
+[pointer_dereference.88] reference is null in *args: SUCCESS
+[pointer_dereference.89] reference is null in *args: SUCCESS
+[pointer_dereference.90] reference is null in *args: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.9] reference is null in *args: SUCCESS
+[pointer_dereference.91] reference is null in *args: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.10] reference is null in array_data_init$10[array_init_iter$11]: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.11] reference is null in *malloc_site$12: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.12] reference is null in *malloc_site$12: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.13] reference is null in *malloc_site$12: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.14] reference is null in *malloc_site$12: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.15] reference is null in *malloc_site$13: SUCCESS
+
+** 0 of 123 failed (1 iteration)
+VERIFICATION SUCCESSFUL
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
index e3aa52b3cef..62ba98812e5 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
-test_parseint_with_radix.class
---refine-strings
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.class b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.class
deleted file mode 100644
index 876f33d861b9addf3ed10e48ee6ee421597834fd..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1141
zcmah|T~E_s7(MU0tzB1O9}0-z2cm347~m9jC?ZNEnVNthfET1}%_xqJv_-uW{{}a5
z$F-V>kp%DkM_wSF7TnN5Y|{35pO5pNbNcqjuWx$*a>%P_Mz4&Ng0zYNGAjCTJpv8=
z(z}C$0~rG<6!a>{N*kPzF{ok)!!m9NBzttnF>KeYTFxWW(U&SlNkA+Jghx%wbngpD
zsr0NsaH3i=1X>EFWjtG7T{7$!Ub8@=P%Y|}S=~0h^-(hDE}M=(N5M55cX3U(9mBNT
z#W$wAylCqs^KG7ptGa0kw5DDbR`l0;wxV0*?2K!hRyptQ=(zTfhu=^YkbTG!%VLU1
z>>REo83lE_%<YpWAPY3jxO(x`Q+>_nO5X&O(PHIDtvXX(w~NN4>1pdajsAegNkbe7
zf!M$Nh&M8MczG>388<cD!ia_z#01*w{o{YUe{9=TTcEptXz)K5=T9Rg<F<x7xce8S
z=SwR_(G@tGYV^@_IbLToWw}P#APvQLmrL*KG>%QB>3K_iZlc07#MYAGn6^=>iK5T$
zItx5N3%Jbl*v!)>V(p#{j3jV(B=}5nmE~LT9m?!Ld}I*789u{)lJpsChYe^&8&?su
z;~X;_7M%o>n0ueu3vOX-7lHYNw1Z%wFBbcX(7jIxZzA5AkUt>03uS%>k?*zKRz0_k
z@yuRm3wa+w^$|kH0iq`WM2`V@#3i5jFzHea1;|vZkaC2-rHU~`@sPDAbYq%M%&}Ub
z4;vKXiOg{(MmIWep5oe&LMOUt#xw?S!OzVxchS#LFfP$qpqqCaLi^~GaYg(@GO&;I
rQOM1EYBuM54}o|>`+}xT$iZy{rOyaATJB+n5YQfYALc3-0bKhHa0Bu3

diff --git a/regression/strings-smoke-tests/java_parselong_1/test_parselong.class b/regression/strings-smoke-tests/java_parselong_1/test_parselong.class
deleted file mode 100644
index d912ed08003c33b066551abc750ef9f2eb82ee74..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 923
zcmZuvU2hUm5IuKUSXh>iLP7kdT9me0N~Msd#Mo4QFsnXbnzTNc3vBS#?QXNX_)C0|
zKj5>Ph_Q*j`=2z<-PR(~Y;t#I?#!Gs=g!aH-@XHAprs>)MGciWZs|~PTSpa32_&%`
z1sLT38dh{9WY!%Wcd@FW#*km+zHfPfa2@}l@Ojs^`V4HJA=Va-2<|gPs!O{J>W<sD
z7&4}CtY^c+uI0Uu$qYHu?QwgTdqVoBK{a?Se1@zUSbp&8h<m<eyUt*X`W$lMFchmV
z%>(|H*KF<#YMsCnbQ|JuZ$Op#bFPVsA9xaRrjqD}Ad>qNhEyluy*E$!QAmemVTiYT
z_US-+#~pe->#>mZ^V1AhWorXj%n|$lVW@F^ZF6&@UT?0qTCJwcThmZCu#S5M(#SBB
zCPmwSm3`!SF7ZxJLuqIj*g$g%=y~_R>IDpi>g<qGp7f->NrEyY!nsfEbBjoh%%o_?
zruQcK`<5>}tA9q31Pg|AL65zU1=^bwZ4Aqn<WOWqXopA>I&<XJ=r4CFx;zH^NQQzu
zov|>;Fi*B|l7Iq=<Rx$cC5p)65mfqs_A!*bTx1N@T=|OV_9w(f$d~7#y?c-3F%o-Y
z=s*66jwVrw83{3qp#3Ifoz^>pI4Xp-MV{nPrX0e-MO>o4PLFgMSBOQ1w*M-w5$o$=
wT=|8HhO%0q`h~M08{q`NTrT+q#t54F0czwkVzUFwHc=?X11ZZ5aunSB13X*2cmMzZ

diff --git a/regression/strings-smoke-tests/java_parselong_2/test_parselong.class b/regression/strings-smoke-tests/java_parselong_2/test_parselong.class
deleted file mode 100644
index d0ba8c19bc710603d76026422fffd27612d95e29..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 926
zcmZuwO>fgc5Pj=7apE}NO$gs9EhK56NlSnOr6LMN0vR|2Rcbk)O=5zJYge|zFX2MO
zodYL8B8W<GN8-2e3qZ`er6HuUv^z69Gw;pw?)Tqcz5;0ChKd9h6<mzsk_riB6%|xt
zh+`>C3GaUVWD5#vDq<q*vWhEMR#0ciEppE@T;FtT?~dv5u4VKY*fv9C&9qH_ogq}I
zZZgPir*AN%bkjB-4tKkT`&cA1WOb*<txfKl!aoek{&Uk~NbA1g`A_$_>lv0~4{lPQ
zU2fV8g~}6shri@?i`#>G$9GLS4RE+Spvv4a$3(^RU4b}LNpu4c!Tml%qT}=4iwAr!
zphL1SMAv%O;XrD~8M-~=t|{o}rWr1a)*8~t5c~gOsBx{)Xm#8Djc1LO)vF?}p<qSB
zD#%G9#Za6Swf-u*;kpj-PEJE9Xll5I>r+6Fx;sYCXUJD(hZOQ8C+&3-lpz+(eP9=k
zDY{oBJyMgZwnaaj^zR#<=^Fhbj-;4Bqyzff+nA?|lc0OU(nT>9Ss@TjWN6KjSErrP
z9$p%Qy(dFLj@C#JWSApcJ4iqt1@dAzfg(jj@f*nW0qgsawz8oyWWAP7e@3|V0g(}M
zr8y|CUL(Gb*wz^8w|}CeNmQVQ0@MP;6%Rut{0tP75ydS+6f8=VLr6G@Q?#q}QcmLx
z@yO5vIE!<{`+N|Wexa<OB<HDi{%Fi*Fawau#y>$DL6P4=4t+#qc4W~e3`x5!gt<VD
GgoQu3{J;_b

diff --git a/regression/strings-smoke-tests/java_parselong_3/test_parselong.class b/regression/strings-smoke-tests/java_parselong_3/test_parselong.class
deleted file mode 100644
index c7cafd723c4e08a94e4da4d1e9e38262fa07c6f8..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 927
zcmZuwT~E_c7=BLIu3OiAvpK(qqT4_ijG-YSk)S4;suwdP;DtHcnprF@X*++3H!j|L
zttQS$qWAtM!S@to&e104yx-6BzUQ1@hu?nyXyT5BBxY3Hh~cIN2^9@h)Z$2BRyjI4
zq!>WOoQAlFx}{+r3o7ai`5Er}rWaVQ<3F%`-nPvy1KVMUu33&1tTRNawJipD)9soJ
zX~S~NXZ^jl>Aeua3^~K?aC?h;me5a(a`4*n88Sv-`oXJx?)j$eI=#D8XOCMBL$UhO
z*yV3|-R4fO-U>X6yde(vdX$+z!%bBDz!QiQnM5}P5!|0JBwGRRym`v^Lpn4ThS*xi
zK50m6xqYu=KC%S;{5Zn}QCdd^Sz`Y`3`1(Zv9!9n*jR3?(AN-wiz=3MG_b5Ag)~EH
zl(q49v=2ScCE}@ZEEP>1E4V#|^t`=mb^?Y%b+St_pVX+lK@(+&hm9Z0#WRu~*JvQ=
zQP!qSCr$^@HGRu7yQds!WI>-Cblf|brkj(bJHs+1(G^J%5KUxh&5>58ozbq$4#7T=
zAR$j{G&C|yk*psFpnxK2ahyYmEF$>>Wcq>i14!Gs$PltIm(jjK+4zj;0QvG1)OYWZ
zI6!=R2<_)T*1^asP$MB~5emssXmrK1h@nDg_ec{g$`nILIFAdoYxGnu;u7)5(hInZ
zE5!S1XqSGYqM|GpD1Z92&1TpGkj*8&LLWetKSGXtL3FZZQAUBJ-xq_qMv8>%e*mr~
BzzhHY

diff --git a/regression/strings-smoke-tests/java_parselong_4/test_parselong.class b/regression/strings-smoke-tests/java_parselong_4/test_parselong.class
deleted file mode 100644
index 89e6a99d4abcb7c4121abf106898def48d7b314c..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 929
zcmZuwOK;Oa5dPM2;>2;@O$hH63Q1aM`bgUYrJ^bzfeajiDzzNYCRqg+*RE`b-@p&x
zLd2ajAQ40*xN+boA%U26A0edjV;(y*-#4?nKmUCF2B3je9Vtv}xE9BC9SSNss;DK9
z#7q?U_2V_Y8fJAQWYi5EH!-K7&QO@<zAwDMavlG!<@1&;It*-wA+}~YR<O<xsn)g_
z)J?Y|7&4~ih{wIXmhhg+V1~Tuwz<8<Jxkh0PBnO8`3zYz5PtA{pL@QrU8j4C>g;jL
zVJKCfnY;WIuiM<|)|-K6(Q1gpy)I=IPFW@@e&9*Ou}q>Hf=KQU8B)!Fw_iTu`ym|~
z3qyRZZ67tHH{G7s7WXYlzc9*hPL?*1MUL424@0iimF33L;==r~l%ew)77Q$6$v_$z
zhVn3P<9N9DJkKTS=}|Nd4Fk(q8Nqte+7<19p;#U7Q%)#7EN{|G84_XZhkEIhqz5$`
zNoJU}Y15w57IcJfd7^W|k%kuZXn{6-2UB!*QgpUhwk*3MEdrv69R2fT)k!jv(U}3*
z2T~Li=pPH63=^aqhXE*}L{<W4P$rK|eg~BvVEq8fc0MwIYR+ckUl85+h*%$m$q8t0
z-XeK`#P$IC_kX<op;w|tLevuIl+&jZehwNch~qXPN*0q8Lr6G_b0l@TEa!27c;x5~
zT*M{feL3_izfsXJsTL`B>ZHv^*aMKuCqKjJLsQ>FjeJ6Eyk%J?3dOi12XloC1y}z9
D$DqOl

diff --git a/regression/strings-smoke-tests/java_parselong_5/test_parselong.class b/regression/strings-smoke-tests/java_parselong_5/test_parselong.class
deleted file mode 100644
index deaff359766878fc996234305ee5403faf397641..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 949
zcmah|%Wl(95Ixti<Hm8`O$hH4+LE-iX=#830a3Lefeb8yDzz-ojbjBD*RE`bFJVLY
z0M>v+5S3uh7qNjb*DVbpl}IGtnYlA_&K!@w|N8P3Km#{5q%f;uZVK}nBwW!@MJ<6O
z7L?&|_=A$5Vo^gvWL?#;gk=?VhQcfl0?Q9=&kZ*1fVUm1!@zbJ;!WGN!#fPIYHf=_
z-tamWL&mUO>v3<dZTU|{GDF_*Ozv!P-xmH+P!3<%0YlaZtss29&;7u1Jhyv``s{Jr
zWhhmj8N2)yuRGlB)?1-((`|&q{Vr7&PPis2LFfy_iAtgyfe7vo8B(o~n=c>n{fG|9
z!Z6h|ouh%Yme=!5>%J}M7seSbi`F`_$PxR0VHoC?R#*Q26ZI=9R&`v%nvOIw4CPU?
z^*@T=^L>xzNsm)d(a>=nH^vA&Y42KQ$WW|K4liU&kJ=j~G(#fN<IpahQ1qZiI%P&x
z8xAc3y_b#^*uK>{=15A0J-VPR*ue}fREk!KWy@kJvSJ{b$k8)TUY$-xr?M~rdryXh
z0zKnVkYSo^{V)MVl*miq6v`A4#cv_gAGm!0X*(YqKsFYY&rsGsAl^rzG7a_h8zc{q
z*d9Rp_E)q&iVDzJ1X_YZb{rZleirmy5LlBuL83xA1ccK#L#Ku{oW(h!k)`kAJT4IJ
yi&0$qiFp+jxk&Xh$5S?<5rAAi`3ZU-s{9Ue>?7in6N@$qB>k??<q|m(F8>CT6U7|>

diff --git a/regression/strings-smoke-tests/java_parselong_binary_1/Test.class b/regression/strings-smoke-tests/java_parselong_binary_1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..199471e4b3e59c46dea1fbe29a3cdce80ba66a28
GIT binary patch
literal 854
zcmah{%Wl(95Ixt=*m0UyW5Tnvv>^$!X=!!@R8&AJ1iDC7sogn_2`<L2Y={3qVncp_
zH6Rg0CD`*tY#_{aO9B)LFYcWg&zy5+=6?P0=`(;PnmRI=SFw=76&(T=bu6KxA&sl@
zcs%|_Nl;PMq4BJmjykTXxXw^qw4%rfV>j@lyKZE4J*UUO_8F9x>$~x72C-V(Wso+5
zp2LuByT0>y@Vx7UJ3N`8&<<?N+qFWM`zJvue(FYq(cW>Q_$FaI2?9E!IOGKf)(flQ
zS$@CKi9^@#Q-X46g;7HNfFaX~E&JIc>o7s1t{74++dI*tcY;A^JNI4Au5p4D4rm~U
zJVWkpaE7JjwblQBynb25ih%}J4a^|RP@aO_`8B3{VHi*s5+_!%X5a?a|DfIO9yoT)
zP^zA8luvSI3fd0*KJ}3Fer%inDB7ygOtRCeO^<fQVD_BI4V~UZ8BHx7&<|SJKIUon
z8QMC_m3c2@i6EKC(^(*|K{umYu8+Xpk|Cf-r;-F2X2~{=6HtOlo`y4%;+K#J4!Cs$
zVXq*LAU&+hA0cnNgEB;MZWijR*GL~h+Z#du@>_H`jdD^kAvGbBtw5(YnnMZ|B5RSy
zMVKT^$2!V5OCGHV=Ww2cT_BHM`gc@RT$D;wb!j56nFt5+h4cp)L#WalNaA}ar~BkE
PG6Z9TPh*Z80hfOQZd#^M

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parselong_5/test_parselong.java b/regression/strings-smoke-tests/java_parselong_binary_1/Test.java
similarity index 76%
rename from regression/strings-smoke-tests/java_parselong_5/test_parselong.java
rename to regression/strings-smoke-tests/java_parselong_binary_1/Test.java
index ac30cc8af83..00b77873c3e 100644
--- a/regression/strings-smoke-tests/java_parselong_5/test_parselong.java
+++ b/regression/strings-smoke-tests/java_parselong_binary_1/Test.java
@@ -1,6 +1,6 @@
-public class test_parselong
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo()
     {
         // -2^35
         String str = new String("-100000000000000000000000000000000000");
diff --git a/regression/strings-smoke-tests/java_parselong_3/test.desc b/regression/strings-smoke-tests/java_parselong_binary_1/test.desc
similarity index 66%
rename from regression/strings-smoke-tests/java_parselong_3/test.desc
rename to regression/strings-smoke-tests/java_parselong_binary_1/test.desc
index fa8ad9ccc48..d7a85429a93 100644
--- a/regression/strings-smoke-tests/java_parselong_3/test.desc
+++ b/regression/strings-smoke-tests/java_parselong_binary_1/test.desc
@@ -1,6 +1,6 @@
-THOROUGH
-test_parselong.class
---refine-strings
+CORE
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong_decimal_1/Test.class b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..98489907514727a836ac1541da4410878245c40f
GIT binary patch
literal 828
zcmZuvO;giQ6g@9VlO|0`X=$yWh=P_XlwzgB&~b237gBUlh8ftsrm+TN!X&A`!-X6B
z2VAQ&){z<A`=4~YFJP<U=H;H7d(S=h<NMDqUja1GFp$NZhHGhDHy~l&zyfaQ$lzuQ
zU=#yrs2I>i)S`hZZfUs9P?+aY<b<&s_|XG5;$6?_F|Y#$wdMM5e2+n{EbcKVTS3oZ
zu-dNgJQ=*~I^nJeX2`b#n|pgabOk<jD)DnSB98X16U7_E@hk}Fjp9%w9P(GZ=5fDY
z>%^h!_bEU<;$f7Oe$0^V#N2+d!;ca+>WU%Vvb|G1Mkg4Aw)4mp)pb!|SrD4YVVWWL
zFFDcGSJv0>*6VAl&1Q2=#4Tx9Hc`Whi78kN<w?^0-{W`~h5@NnL;($T6RWuM7yZ-j
zp<~Ak#md=+#Kfj1r0u}(lh&li6Z^kO)VeiE+VW^M45gkExuMe=3!~x01NuRGIlvsP
zI7`cAxw2@5ESc6#lb|<Gs77D0{#11Y_MQw01$x!Q$uL8<c@lskN`!Qr8z;YpLUcgu
z7}9=T9zofzenx8Z1Jof3vop}%yhY|1`u+&Uw?DkYiC5H=lbR*aDN<#FF401o4phem
zA)%o}x(u3d8RrRESi%KdBwd#X(LMjbf`-dVk+QCg)in~`z;r(I3FZ)*@(zmp5$f4C
Q1x*T)xhaM*OF+WaUyl8qtpET3

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parselong_1/test_parselong.java b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.java
similarity index 74%
rename from regression/strings-smoke-tests/java_parselong_1/test_parselong.java
rename to regression/strings-smoke-tests/java_parselong_decimal_1/Test.java
index a328af58250..a46474b1ac4 100644
--- a/regression/strings-smoke-tests/java_parselong_1/test_parselong.java
+++ b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.java
@@ -1,6 +1,6 @@
-public class test_parselong
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo()
     {
         // 2^40
         String str = new String("1099511627776");
diff --git a/regression/strings-smoke-tests/java_parselong_1/test.desc b/regression/strings-smoke-tests/java_parselong_decimal_1/test.desc
similarity index 70%
rename from regression/strings-smoke-tests/java_parselong_1/test.desc
rename to regression/strings-smoke-tests/java_parselong_decimal_1/test.desc
index fa8ad9ccc48..baaacde7d66 100644
--- a/regression/strings-smoke-tests/java_parselong_1/test.desc
+++ b/regression/strings-smoke-tests/java_parselong_decimal_1/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
-test_parselong.class
---refine-strings
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong_decimal_2/Test.class b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..922b885b7b3405849f548cb171d8829a565fd3af
GIT binary patch
literal 832
zcmZuv%Wl(95IxuNBX*p3W5Tl(3VA@9)(wk_QWX`DpeZa;Rcd#RV}eVtE8F2i5F7FX
ztO1E2D#4zAqGhgI5}<f-@67njnKLu@$I;hs09t5iNMlaHwIr@<5HPRd25zcIp&}h0
z9}xynP}QJvR82!2w-nrFD9&49=me4Ld*K5&w7LVQ$H4X&<W<*mqcw&^wYI|`ZumWi
zA=`F6=jrfO*9o>cn4!@2ZELV&1upkbgJSf;4T+<@?S#=?;&|@+bcRvD6ZWmwR&!u^
z{bnZ$T(3_6`M?Uoxbzc-bSJXxms{3B%tl=?Bv<XhsUEH44+GnI<nrn&FR;J~b>xs|
z$o)&skZG7pD=UlUvU!I-lLH$H7IZYRs3U_cLwTBY|Mxr|27ym<MP5O{k`5EgfAK%-
z?mKqGP^zBoh>t8YC2jj&pTx#Zp4i5Jk{;Kn`Rp`nV?fJcFnUht22O9HjK&iU=?86Q
z4|BBSG_9BA%Dfk{5+Iq#(^(*|NjIZgs*k}wkRhN*ryK_vX2{l004TvAPsO=O@*9Xm
z2do`J*exW+5I5^N?F*#!kB~<w&dxx2`wpo?sJmlm-~Wh?rcqus5mz-Jku5``*O*5V
z6{>cRJg&kZWg5NZGR~8iM*|mdk(6B`kKXi8R1{nmOO$nGqOTPzCv+k88Ttr{_#R^7
V6XdgvavBMOzRt%nOOAl6zW`}>p+5is

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parselong_3/test_parselong.java b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.java
similarity index 75%
rename from regression/strings-smoke-tests/java_parselong_3/test_parselong.java
rename to regression/strings-smoke-tests/java_parselong_decimal_2/Test.java
index e05341bdb86..e5578284020 100644
--- a/regression/strings-smoke-tests/java_parselong_3/test_parselong.java
+++ b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.java
@@ -1,6 +1,6 @@
-public class test_parselong
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo()
     {
         // -2^41
         String str = new String("-2199023255552");
diff --git a/regression/strings-smoke-tests/java_parselong_5/test.desc b/regression/strings-smoke-tests/java_parselong_decimal_2/test.desc
similarity index 70%
rename from regression/strings-smoke-tests/java_parselong_5/test.desc
rename to regression/strings-smoke-tests/java_parselong_decimal_2/test.desc
index fa8ad9ccc48..baaacde7d66 100644
--- a/regression/strings-smoke-tests/java_parselong_5/test.desc
+++ b/regression/strings-smoke-tests/java_parselong_decimal_2/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
-test_parselong.class
---refine-strings
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong_hex_1/Test.class b/regression/strings-smoke-tests/java_parselong_hex_1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..33ba81a040629e141776f69a38248f9fb51f07b5
GIT binary patch
literal 831
zcmZuv%Wl(95Ixti<JfT;CuvN0meN8VrA^vqN2ywcA_1XYq^i{JoY)O6#;$CK4?%3m
z53pbbNCZ&{_DFmSUjSmRTN0pb?wy%CbIzHW`}OCi&j6Zes>ong#*Gx_R0x<?aTB)`
zq*0bA;mx=2Y)(c+g~GF{Dr#7eahstqZ-${AM2_!;_ngq|y0*o@4j7Vaj^{+{42ep0
zk3nqtmd%iDJD$Bgc-FOpU7pO4Z~Hyd-7^D+`)5Hhdg6qH(cZPg=ni2V`aYdu6!3y0
z^SN1fO|M_?M1kY=DIs}m24PJ7kRj8F%-++-=5dThT`{EAdhVGXwc`(ho_*ip><TAX
z;(!`-<QVjS!3l1m(b(*^tgXYw^2#dDTa>Y+p^k=zDP$Q+lcLSv<JbxUpVW$+K*q9$
z6|DXRztcUkdl5sia=sxxv8f4Y+xPmUHSY1$HvUueph~@GCsi$%cEey;cIX7QHC9H`
zi3apQi#fn7?Knd#W_pSDLRJDK6FEBb<kjhBbW61n*jq9L6zELGL569vwbKL?VUVZb
z!npVaM1lj>Pay2)6C;R^YP$Xr(#AU^hbYWULw@-R=@TgXBdA~ghz=)F&YFl>4e;M6
zK_&hiWR#J@U1H=a3{s}jS1#cqc{wcN5-yXnE9B9a{(-WLt74HVu8s9IW95{cPk(?m
age<;>n0Sxm`9?X61VP*2<Cq~w!1Z6RtD!{z

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parselong_2/test_parselong.java b/regression/strings-smoke-tests/java_parselong_hex_1/Test.java
similarity index 73%
rename from regression/strings-smoke-tests/java_parselong_2/test_parselong.java
rename to regression/strings-smoke-tests/java_parselong_hex_1/Test.java
index c2e3d60bd11..944597ee24c 100644
--- a/regression/strings-smoke-tests/java_parselong_2/test_parselong.java
+++ b/regression/strings-smoke-tests/java_parselong_hex_1/Test.java
@@ -1,6 +1,6 @@
-public class test_parselong
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo()
     {
         String str = new String("+00AbCdEf0123");
         long parsed = Long.parseLong(str, 16);
diff --git a/regression/strings-smoke-tests/java_parselong_4/test.desc b/regression/strings-smoke-tests/java_parselong_hex_1/test.desc
similarity index 66%
rename from regression/strings-smoke-tests/java_parselong_4/test.desc
rename to regression/strings-smoke-tests/java_parselong_hex_1/test.desc
index 17db69e3979..f9ef9a9c0b6 100644
--- a/regression/strings-smoke-tests/java_parselong_4/test.desc
+++ b/regression/strings-smoke-tests/java_parselong_hex_1/test.desc
@@ -1,6 +1,6 @@
-THOROUGH
-test_parselong.class
---refine-strings
+CORE
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong_octal_1/Test.class b/regression/strings-smoke-tests/java_parselong_octal_1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..73fbc420bb0eb1386ccc9ff51728b20ff4ef2053
GIT binary patch
literal 834
zcmZuv%Wl(95Ir|`?AURdS7XAn6bgAjn?3?8C{<Al5^aD*s!Hwd#xcRg*p=<@4XhCx
z@&l{^i6AP$js>5D1Y)k+CP0yrduPTo=bV{4-+z7n0-%Yejtr(%TuR}xjs#|OT)|Zh
zX;hNHk8dyOr=qGu6InGKbzD<%ouN3x!_W>Q$M?c@C*&R1?lQ1l24&gtoM?qXs@Ap{
z<Tbx*Gh|ziXFuvc@7TeXNM<Ose2cr=JaB}66qKW<PDmK7Ejx^E6UGzYr!$NKQLx8f
z@P^C1UZWiaj@P3EWuFIOOufO7X-C|8_K@$#Xw(%$YT0s+^yqEBA6WK%N3d&xU`_xU
z$RW>=`xl%-w{G5OE-fz1AKxN%R>how2IdV+Aj?o5*WEpy$h{!&Nw6$9R4f=+#L{03
zk2`y|6)}{mCwme@n;3((e6L4x<2Da%^FKuoYSeyqT(#!X^DvlQJ9GlOJ5ojiiu&|{
z-ewom^voGr1C}d`UdWO_GLfgVKwg7xMt8D41batD0!2ENILI(bwsDw%5=`<moEjCs
zf=qD0$^jBP1!)L*vz|+RLUQ#zlmUuUlTcs3LHYpN&Jg<7Kca(iRIo}hs|i|2`s>7>
zhl&bPxI>IWg-ObE+U7D&lb6RV&fqL5J4YUE^-ok(oR>>fabcvd87rskLi!_&0aW=d
XWa$HxlZ^_PBofA|7{?Sj30(XQv3{dB

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/java_parselong_4/test_parselong.java b/regression/strings-smoke-tests/java_parselong_octal_1/Test.java
similarity index 74%
rename from regression/strings-smoke-tests/java_parselong_4/test_parselong.java
rename to regression/strings-smoke-tests/java_parselong_octal_1/Test.java
index 67eee61b85a..4dc8f7b712a 100644
--- a/regression/strings-smoke-tests/java_parselong_4/test_parselong.java
+++ b/regression/strings-smoke-tests/java_parselong_octal_1/Test.java
@@ -1,6 +1,6 @@
-public class test_parselong
+public class Test
 {
-    public static void main(String[] args)
+    public static void foo()
     {
         String str = new String("7654321076543210");
         long parsed = Long.parseLong(str, 8);
diff --git a/regression/strings-smoke-tests/java_parselong_2/test.desc b/regression/strings-smoke-tests/java_parselong_octal_1/test.desc
similarity index 66%
rename from regression/strings-smoke-tests/java_parselong_2/test.desc
rename to regression/strings-smoke-tests/java_parselong_octal_1/test.desc
index 17db69e3979..f9ef9a9c0b6 100644
--- a/regression/strings-smoke-tests/java_parselong_2/test.desc
+++ b/regression/strings-smoke-tests/java_parselong_octal_1/test.desc
@@ -1,6 +1,6 @@
-THOROUGH
-test_parselong.class
---refine-strings
+CORE
+Test.class
+--refine-strings --function Test.foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp
index 3110c454607..1801ec16c22 100644
--- a/src/solvers/refinement/string_constraint_generator_valueof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp
@@ -415,91 +415,97 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
 
 /// add axioms corresponding to the Integer.parseInt java function
 /// \param f: a function application with either one string expression or one
-///   string expression and an expression for the radix
+///   string expression and an integer expression for the radix
 /// \return an integer expression
 exprt string_constraint_generatort::add_axioms_for_parse_int(
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2);
-  string_exprt str=get_string_expr(f.arguments()[0]);
+  const string_exprt str=get_string_expr(f.arguments()[0]);
+  const typet &type=f.type();
+  PRECONDITION(type.id()==ID_signedbv);
   const exprt radix=
     f.arguments().size()==1?
-      static_cast<exprt>(from_integer(10, f.type())):
-      static_cast<exprt>(typecast_exprt(f.arguments()[1], f.type()));
+      static_cast<exprt>(from_integer(10, type)):
+      static_cast<exprt>(typecast_exprt(f.arguments()[1], type));
 
-  const typet &type=f.type();
-  symbol_exprt i=fresh_symbol("parsed_int", type);
+  const symbol_exprt x=fresh_symbol("parsed_int", type);
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
   const typet &char_type=ref_type.get_char_type();
-  exprt minus_char=constant_char('-', char_type);
-  exprt plus_char=constant_char('+', char_type);
-  PRECONDITION(type.id()==ID_signedbv);
+  const typet &index_type=ref_type.get_index_type();
+  const exprt minus_char=constant_char('-', char_type);
+  const exprt zero_expr=from_integer(0, type);
 
-  exprt chr=str[0];
-  exprt starts_with_minus=equal_exprt(chr, minus_char);
-  exprt starts_with_plus=equal_exprt(chr, plus_char);
-  exprt starts_with_digit=
-    not_exprt(or_exprt(starts_with_minus, starts_with_plus));
+  /// We experimented with making the max_string_length depend on the base, but
+  /// this did not make any difference to the speed of execution.
+  const std::size_t max_string_length=to_bitvector_type(type).get_width()+1;
 
   /// TODO: we should throw an exception when this does not hold:
-  const std::size_t max_string_length=40;
+  /// Note that the only thing stopping us from taking longer strings with many
+  /// leading zeros is the axioms for correct number format
   add_axioms_for_correct_number_format(str, radix, max_string_length);
 
-  /// TODO(OJones): size should depend on the radix
-  /// TODO(OJones): we should deal with overflow properly
-  for(std::size_t size=1; size<=max_string_length; size++)
-  {
-    exprt sum=from_integer(0, type);
-    exprt first_value=get_numeric_value_from_character(chr, char_type, type);
-    equal_exprt premise=str.axiom_for_has_length(size);
+  /// TODO(OJones): Fix the below algorithm to make it work for min_int. There
+  /// are two problems. (1) Because we build i as positive and then negate it if
+  /// the first character is '-', we hit overflow for min_int because
+  /// |min_int| > max_int. (2) radix^63 overflows. I think we'll have to
+  /// special-case it.
 
-    for(std::size_t j=1; j<size; j++)
-    {
-      mult_exprt radix_sum(sum, radix);
-      if(j>=max_string_length-1)
-      {
-        // We have to be careful about overflows
-        div_exprt div(sum, radix);
-        implies_exprt no_overflow(premise, (equal_exprt(div, sum)));
-        axioms.push_back(no_overflow);
-      }
+  axioms.push_back(binary_relation_exprt(x, ID_ge, zero_expr));
 
-      sum=plus_exprt_with_overflow_check(
-        radix_sum,
-        get_numeric_value_from_character(str[j], char_type, type));
+  exprt radix_to_power_of_i;
+  exprt no_overflow;
 
-      mult_exprt first(first_value, radix);
-      if(j>=max_string_length-1)
-      {
-        // We have to be careful about overflows
-        div_exprt div_first(first, radix);
-        implies_exprt no_overflow_first(
-          and_exprt(starts_with_digit, premise),
-          equal_exprt(div_first, first_value));
-        axioms.push_back(no_overflow_first);
-      }
-      first_value=first;
-    }
+  for(std::size_t i=0; i<max_string_length; ++i)
+  {
+    /// We are counting backwards from the end of the string, i.e. i refers
+    /// to str[j] where j=str.length()-i-1
+    const constant_exprt i_expr=from_integer(i, index_type);
+    const minus_exprt j(
+      minus_exprt(str.length(), i_expr), from_integer(1, index_type));
 
-    // If the length is `size`, we add axioms:
-    // a1 : starts_with_digit => i=sum+first_value
-    // a2 : starts_with_plus => i=sum
-    // a3 : starts_with_minus => i=-sum
+    if(i==0)
+    {
+      no_overflow=true_exprt();
+      radix_to_power_of_i=from_integer(1, type);
+    }
+    else
+    {
+      exprt radix_to_power_of_i_minus_one=radix_to_power_of_i;
+      /// Note that power_exprt is probably designed for floating point. Also,
+      /// it doesn't work when the exponent isn't a constant, hence why this
+      /// loop is indexed by i instead of j. It is faster than
+      /// mult_exprt(radix_to_power_of_i, radix).
+      radix_to_power_of_i=power_exprt(radix, i_expr);
+      /// The first time there is overflow we will have that
+      /// radix^i/radix != radix^(i-1)
+      /// However, that condition may hold in future, so we have to be sure to
+      /// propagate the first time this fails to all higher values of i
+      no_overflow=and_exprt(
+        equal_exprt(
+          div_exprt(radix_to_power_of_i, radix), radix_to_power_of_i_minus_one),
+        no_overflow);
+    }
 
-    implies_exprt a1(
-      and_exprt(premise, starts_with_digit),
-      equal_exprt(i, plus_exprt(sum, first_value)));
-    axioms.push_back(a1);
+    /// If we have already read all characters from the string then we use 0
+    /// instead of the value from str[j]
+    const binary_relation_exprt i_is_valid(i_expr, ID_lt, str.length());
+    const if_exprt digit_value(
+      i_is_valid,
+      get_numeric_value_from_character(str[j], char_type, type),
+      from_integer(0, type));
 
-    implies_exprt a2(and_exprt(premise, starts_with_plus), equal_exprt(i, sum));
-    axioms.push_back(a2);
+    /// when there is no overflow, str[j] = (x/radix^i)%radix
+    const equal_exprt contribution_of_str_j(
+      digit_value,
+      mod_exprt(div_exprt(x, radix_to_power_of_i), radix));
 
-    implies_exprt a3(
-      and_exprt(premise, starts_with_minus),
-      equal_exprt(i, unary_minus_exprt(sum)));
-    axioms.push_back(a3);
+    axioms.push_back(implies_exprt(no_overflow, contribution_of_str_j));
+    axioms.push_back(implies_exprt(
+      not_exprt(no_overflow), equal_exprt(digit_value, zero_expr)));
   }
-  return i;
+
+  return if_exprt(equal_exprt(str[0], minus_char), unary_minus_exprt(x), x);
 }
 
 /// Check if a character is a digit with respect to the given radix, e.g. if the
@@ -541,7 +547,7 @@ exprt is_digit_with_radix(exprt chr, exprt radix)
 }
 
 /// Get the numeric value of a character, assuming that the radix is large
-/// enough
+/// enough. '+' and '-' yield 0.
 /// \param chr: the character to get the numeric value of
 /// \param char_type: the type to use for characters
 /// \param type: the type to use for the return value
@@ -555,16 +561,25 @@ exprt get_numeric_value_from_character(
   constant_exprt A_char=from_integer('A', char_type);
   constant_exprt ten_int=from_integer(10, char_type);
 
-  binary_relation_exprt upper_case(chr, ID_ge, A_char);
+  /// There are four cases, which occur in ASCII in the following order:
+  /// '+' and '-', digits, upper case letters, lower case letters
   binary_relation_exprt lower_case(chr, ID_ge, a_char);
+  binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
+  binary_relation_exprt upper_case_lower_case_or_digit(chr, ID_ge, zero_char);
 
+  /// return char >= 'a' ? (char - 'a' + 10) :
+  ///   char >= 'A' ? (char - 'A' + 10) :
+  ///     char >= '0' ? (char - '0') : 0
   return typecast_exprt(
     if_exprt(
       lower_case,
       plus_exprt(minus_exprt(chr, a_char), ten_int),
       if_exprt(
-        upper_case,
+        upper_case_or_lower_case,
         plus_exprt(minus_exprt(chr, A_char), ten_int),
-        minus_exprt(chr, zero_char))),
+        if_exprt(
+          upper_case_lower_case_or_digit,
+          minus_exprt(chr, zero_char),
+          from_integer(0, char_type)))),
     type);
 }

From 448abb62a4905f43e7860d352799943d896fa505 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Wed, 26 Jul 2017 14:04:22 +0100
Subject: [PATCH 4/6] Refactor helper functions

---
 .../string_constraint_generator_valueof.cpp   | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp
index 1801ec16c22..f192b47de43 100644
--- a/src/solvers/refinement/string_constraint_generator_valueof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp
@@ -365,7 +365,7 @@ string_exprt string_constraint_generatort::add_axioms_for_value_of(
 /// \param radix: the radix
 /// \param max_size: maximum number of characters
 void string_constraint_generatort::add_axioms_for_correct_number_format(
-  const string_exprt &str, const exprt &radix, std::size_t max_size)
+  const string_exprt &str, const exprt &radix_char_type, std::size_t max_size)
 {
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
   const typet &char_type=ref_type.get_char_type();
@@ -378,7 +378,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
   exprt chr=str[0];
   equal_exprt starts_with_minus(chr, minus_char);
   equal_exprt starts_with_plus(chr, plus_char);
-  exprt starts_with_digit=is_digit_with_radix(chr, radix);
+  exprt starts_with_digit=is_digit_with_radix(chr, radix_char_type);
 
   // TODO: we should have implications in the other direction for correct
   // correct => |str| > 0
@@ -408,7 +408,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
     /// index < length && correct => is_digit(str[index])
     implies_exprt character_at_index_is_digit(
       binary_relation_exprt(index_expr, ID_lt, str.length()),
-      is_digit_with_radix(str[index], radix));
+      is_digit_with_radix(str[index], radix_char_type));
     axioms.push_back(character_at_index_is_digit);
   }
 }
@@ -443,7 +443,8 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
   /// TODO: we should throw an exception when this does not hold:
   /// Note that the only thing stopping us from taking longer strings with many
   /// leading zeros is the axioms for correct number format
-  add_axioms_for_correct_number_format(str, radix, max_string_length);
+  add_axioms_for_correct_number_format(
+    str, typecast_exprt(radix, char_type), max_string_length);
 
   /// TODO(OJones): Fix the below algorithm to make it work for min_int. There
   /// are two problems. (1) Because we build i as positive and then negate it if
@@ -513,21 +514,21 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
 /// \param chr: the character
 /// \param radix:  the radix
 /// \return an expression for the condition
-exprt is_digit_with_radix(exprt chr, exprt radix)
+exprt is_digit_with_radix(exprt chr, exprt radix_char_type)
 {
   const typet &char_type=chr.type();
   exprt zero_char=from_integer('0', char_type);
   exprt nine_char=from_integer('9', char_type);
   exprt a_char=from_integer('a', char_type);
   exprt A_char=from_integer('A', char_type);
+  constant_exprt ten_char_type=from_integer(10, char_type);
 
   and_exprt is_digit_when_radix_le_10(
     binary_relation_exprt(chr, ID_ge, zero_char),
     binary_relation_exprt(
-      chr, ID_lt, plus_exprt(zero_char, typecast_exprt(radix, char_type))));
+      chr, ID_lt, plus_exprt(zero_char, radix_char_type)));
 
-  minus_exprt radix_minus_ten(
-    typecast_exprt(radix, char_type), from_integer(10, char_type));
+  minus_exprt radix_minus_ten(radix_char_type, ten_char_type);
 
   or_exprt is_digit_when_radix_gt_10(
     and_exprt(
@@ -541,7 +542,7 @@ exprt is_digit_with_radix(exprt chr, exprt radix)
       binary_relation_exprt(chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
 
   return if_exprt(
-    binary_relation_exprt(radix, ID_le, from_integer(10, radix.type())),
+    binary_relation_exprt(radix_char_type, ID_le, ten_char_type),
     is_digit_when_radix_le_10,
     is_digit_when_radix_gt_10);
 }

From 7aaf76191b50184906147123512677e2694d3cb2 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Wed, 26 Jul 2017 15:27:01 +0100
Subject: [PATCH 5/6] Refactor big for loop into a function

---
 .../refinement/string_constraint_generator.h  |  10 +-
 .../string_constraint_generator_valueof.cpp   | 101 +++++++++++-------
 2 files changed, 73 insertions(+), 38 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index a4c5c543d1d..659091b7aa6 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -293,9 +293,17 @@ class string_constraint_generatort
   exprt add_axioms_for_offset_by_code_point(
     const function_application_exprt &f);
 
-  exprt add_axioms_for_parse_int(const function_application_exprt &f);
+  exprt add_axioms_for_characters_in_integer_string(
+    const symbol_exprt& x,
+    const typet& type,
+    const typet& char_type,
+    const typet& index_type,
+    const string_exprt& str,
+    const std::size_t max_string_length,
+    const exprt& radix);
   void add_axioms_for_correct_number_format(
     const string_exprt &str, const exprt &radix, std::size_t max_size);
+  exprt add_axioms_for_parse_int(const function_application_exprt &f);
   exprt add_axioms_for_to_char_array(const function_application_exprt &f);
   exprt add_axioms_for_compare_to(const function_application_exprt &f);
 
diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp
index f192b47de43..f3338d36f4b 100644
--- a/src/solvers/refinement/string_constraint_generator_valueof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp
@@ -413,47 +413,35 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
   }
 }
 
-/// add axioms corresponding to the Integer.parseInt java function
-/// \param f: a function application with either one string expression or one
-///   string expression and an integer expression for the radix
-/// \return an integer expression
-exprt string_constraint_generatort::add_axioms_for_parse_int(
-  const function_application_exprt &f)
+/// Add axioms connecting the characters in the input string to the value of the
+/// output integer
+/// \param x: symbol for abs(integer represented by str)
+/// \param type: the type for x
+/// \param char_type: the type to use for characters
+/// \param index_type: the type to use for indexes
+/// \param str: input string
+/// \param max_string_length: the maximum length str can have
+/// \param radix: the radix, with the same type as x
+/// \return an expression for the integer represented by the string
+exprt string_constraint_generatort::add_axioms_for_characters_in_integer_string(
+  const symbol_exprt& x,
+  const typet& type,
+  const typet& char_type,
+  const typet& index_type,
+  const string_exprt& str,
+  const std::size_t max_string_length,
+  const exprt& radix)
 {
-  PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2);
-  const string_exprt str=get_string_expr(f.arguments()[0]);
-  const typet &type=f.type();
-  PRECONDITION(type.id()==ID_signedbv);
-  const exprt radix=
-    f.arguments().size()==1?
-      static_cast<exprt>(from_integer(10, type)):
-      static_cast<exprt>(typecast_exprt(f.arguments()[1], type));
-
-  const symbol_exprt x=fresh_symbol("parsed_int", type);
-  const refined_string_typet &ref_type=to_refined_string_type(str.type());
-  const typet &char_type=ref_type.get_char_type();
-  const typet &index_type=ref_type.get_index_type();
-  const exprt minus_char=constant_char('-', char_type);
-  const exprt zero_expr=from_integer(0, type);
-
-  /// We experimented with making the max_string_length depend on the base, but
-  /// this did not make any difference to the speed of execution.
-  const std::size_t max_string_length=to_bitvector_type(type).get_width()+1;
-
-  /// TODO: we should throw an exception when this does not hold:
-  /// Note that the only thing stopping us from taking longer strings with many
-  /// leading zeros is the axioms for correct number format
-  add_axioms_for_correct_number_format(
-    str, typecast_exprt(radix, char_type), max_string_length);
-
   /// TODO(OJones): Fix the below algorithm to make it work for min_int. There
   /// are two problems. (1) Because we build i as positive and then negate it if
   /// the first character is '-', we hit overflow for min_int because
   /// |min_int| > max_int. (2) radix^63 overflows. I think we'll have to
   /// special-case it.
 
+  const exprt zero_expr=from_integer(0, type);
   axioms.push_back(binary_relation_exprt(x, ID_ge, zero_expr));
 
+  const exprt one_index_type=from_integer(1, index_type);
   exprt radix_to_power_of_i;
   exprt no_overflow;
 
@@ -462,8 +450,7 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
     /// We are counting backwards from the end of the string, i.e. i refers
     /// to str[j] where j=str.length()-i-1
     const constant_exprt i_expr=from_integer(i, index_type);
-    const minus_exprt j(
-      minus_exprt(str.length(), i_expr), from_integer(1, index_type));
+    const minus_exprt j(minus_exprt(str.length(), i_expr), one_index_type);
 
     if(i==0)
     {
@@ -472,7 +459,7 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
     }
     else
     {
-      exprt radix_to_power_of_i_minus_one=radix_to_power_of_i;
+      const exprt radix_to_power_of_i_minus_one=radix_to_power_of_i;
       /// Note that power_exprt is probably designed for floating point. Also,
       /// it doesn't work when the exponent isn't a constant, hence why this
       /// loop is indexed by i instead of j. It is faster than
@@ -494,7 +481,7 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
     const if_exprt digit_value(
       i_is_valid,
       get_numeric_value_from_character(str[j], char_type, type),
-      from_integer(0, type));
+      zero_expr);
 
     /// when there is no overflow, str[j] = (x/radix^i)%radix
     const equal_exprt contribution_of_str_j(
@@ -506,7 +493,47 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
       not_exprt(no_overflow), equal_exprt(digit_value, zero_expr)));
   }
 
-  return if_exprt(equal_exprt(str[0], minus_char), unary_minus_exprt(x), x);
+  return if_exprt(
+    equal_exprt(str[0], constant_char('-', char_type)),
+    unary_minus_exprt(x),
+    x);
+}
+
+/// add axioms corresponding to the Integer.parseInt java function
+/// \param f: a function application with either one string expression or one
+///   string expression and an integer expression for the radix
+/// \return an integer expression
+exprt string_constraint_generatort::add_axioms_for_parse_int(
+  const function_application_exprt &f)
+{
+  PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2);
+  const string_exprt str=get_string_expr(f.arguments()[0]);
+  const typet &type=f.type();
+  PRECONDITION(type.id()==ID_signedbv);
+  const exprt radix=
+    f.arguments().size()==1?
+      static_cast<exprt>(from_integer(10, type)):
+      static_cast<exprt>(typecast_exprt(f.arguments()[1], type));
+
+  const symbol_exprt x=fresh_symbol("abs_parsed_int", type);
+  const refined_string_typet &ref_type=to_refined_string_type(str.type());
+  const typet &char_type=ref_type.get_char_type();
+  const typet &index_type=ref_type.get_index_type();
+
+  /// We experimented with making the max_string_length depend on the base, but
+  /// this did not make any difference to the speed of execution.
+  const std::size_t max_string_length=to_bitvector_type(type).get_width()+1;
+
+  /// TODO: we should throw an exception when this does not hold:
+  /// Note that the only thing stopping us from taking longer strings with many
+  /// leading zeros is the axioms for correct number format
+  add_axioms_for_correct_number_format(
+    str, typecast_exprt(radix, char_type), max_string_length);
+
+  exprt parsed_int_expr=add_axioms_for_characters_in_integer_string(
+    x, type, char_type, index_type, str, max_string_length, radix);
+
+  return parsed_int_expr;
 }
 
 /// Check if a character is a digit with respect to the given radix, e.g. if the

From 4cfbfb5556a355737035533e437481c275ca83a8 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Thu, 27 Jul 2017 11:40:54 +0100
Subject: [PATCH 6/6] Updated two unit tests

---
 .../get_numeric_value_from_character.cpp      | 108 +++++++++++++++---
 .../is_digit_with_radix.cpp                   |  47 +++-----
 2 files changed, 103 insertions(+), 52 deletions(-)

diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
index d562cb1c5ac..296c8780523 100644
--- a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
+++ b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
@@ -15,27 +15,97 @@
 #include <util/simplify_expr.h>
 #include <util/std_types.h>
 
+
+
 SCENARIO("get_numeric_value_from_character",
   "[core][solvers][refinement][string_constraint_generator_valueof]")
 {
-  typet char_type=unsignedbv_typet(16);
-  typet int_type=signedbv_typet(32);
+  const typet char_type_1=unsignedbv_typet(8);
+  const typet char_type_2=unsignedbv_typet(16);
+  const typet char_type_3=unsignedbv_typet(32);
+  const typet int_type_1=signedbv_typet(8);
+  const typet int_type_2=signedbv_typet(16);
+  const typet int_type_3=signedbv_typet(32);
+  const typet int_type_4=signedbv_typet(64);
   symbol_tablet symtab;
-  namespacet ns(symtab);
-
-  REQUIRE(from_integer(0, int_type)==simplify_expr(
-    get_numeric_value_from_character(
-      from_integer('0', char_type), char_type, int_type), ns));
-  REQUIRE(from_integer(9, int_type)==simplify_expr(
-    get_numeric_value_from_character(
-      from_integer('9', char_type),
-      char_type, int_type), ns));
-  REQUIRE(from_integer(10, int_type)==simplify_expr(
-    get_numeric_value_from_character(
-      from_integer('A', char_type),
-      char_type, int_type), ns));
-  REQUIRE(from_integer(35, int_type)==simplify_expr(
-    get_numeric_value_from_character(
-      from_integer('z', char_type),
-      char_type, int_type), ns));
+  const namespacet ns(symtab);
+
+  WHEN("0")
+  {
+    mp_integer character='0';
+    mp_integer expected_value=0;
+    const typet& char_type=char_type_1;
+    const typet& int_type=int_type_1;
+    constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
+    exprt actual_value_exprt=simplify_expr(
+      get_numeric_value_from_character(
+        from_integer(character, char_type), char_type, int_type),
+      ns);
+    REQUIRE(expected_value_exprt==actual_value_exprt);
+  }
+  WHEN("9")
+  {
+    mp_integer character='9';
+    mp_integer expected_value=9;
+    const typet& char_type=char_type_2;
+    const typet& int_type=int_type_2;
+    constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
+    exprt actual_value_exprt=simplify_expr(
+      get_numeric_value_from_character(
+        from_integer(character, char_type), char_type, int_type),
+      ns);
+    REQUIRE(expected_value_exprt==actual_value_exprt);
+  }
+  WHEN("A")
+  {
+    mp_integer character='A';
+    mp_integer expected_value=10;
+    const typet& char_type=char_type_3;
+    const typet& int_type=int_type_3;
+    constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
+    exprt actual_value_exprt=simplify_expr(
+      get_numeric_value_from_character(
+        from_integer(character, char_type), char_type, int_type),
+      ns);
+    REQUIRE(expected_value_exprt==actual_value_exprt);
+  }
+  WHEN("z")
+  {
+    mp_integer character='z';
+    mp_integer expected_value=35;
+    const typet& char_type=char_type_1;
+    const typet& int_type=int_type_4;
+    constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
+    exprt actual_value_exprt=simplify_expr(
+      get_numeric_value_from_character(
+        from_integer(character, char_type), char_type, int_type),
+      ns);
+    REQUIRE(expected_value_exprt==actual_value_exprt);
+  }
+  WHEN("+")
+  {
+    mp_integer character='+';
+    mp_integer expected_value=0;
+    const typet& char_type=char_type_2;
+    const typet& int_type=int_type_1;
+    constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
+    exprt actual_value_exprt=simplify_expr(
+      get_numeric_value_from_character(
+        from_integer(character, char_type), char_type, int_type),
+      ns);
+    REQUIRE(expected_value_exprt==actual_value_exprt);
+  }
+  WHEN("-")
+  {
+    mp_integer character='-';
+    mp_integer expected_value=0;
+    const typet& char_type=char_type_3;
+    const typet& int_type=int_type_2;
+    constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
+    exprt actual_value_exprt=simplify_expr(
+      get_numeric_value_from_character(
+        from_integer(character, char_type), char_type, int_type),
+      ns);
+    REQUIRE(expected_value_exprt==actual_value_exprt);
+  }
 }
diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp
index 85a14ff3859..31ca819a600 100644
--- a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp
+++ b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp
@@ -18,57 +18,38 @@
 SCENARIO("is_digit_with_radix",
   "[core][solvers][refinement][string_constraint_generator_valueof]")
 {
-  typet char_type=unsignedbv_typet(16);
-  typet int_type=signedbv_typet(32);
+  const typet char_type=unsignedbv_typet(16);
   symbol_tablet symtab;
-  namespacet ns(symtab);
+  const namespacet ns(symtab);
 
   WHEN("Radix 10")
   {
-    int radix=10;
+    const constant_exprt radix_expr=from_integer(10, char_type);
     REQUIRE(true_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('0', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('0', char_type), radix_expr), ns));
     REQUIRE(true_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('9', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('9', char_type), radix_expr), ns));
     REQUIRE(false_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('a', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('a', char_type), radix_expr), ns));
   }
   WHEN("Radix 8")
   {
-    int radix=8;
+    const constant_exprt radix_expr=from_integer(8, char_type);
     REQUIRE(true_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('7', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('7', char_type), radix_expr), ns));
     REQUIRE(false_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('8', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('8', char_type), radix_expr), ns));
   }
   WHEN("Radix 16")
   {
-    int radix=16;
+    const constant_exprt radix_expr=from_integer(16, char_type);
     REQUIRE(true_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('a', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('a', char_type), radix_expr), ns));
     REQUIRE(true_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('A', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('A', char_type), radix_expr), ns));
     REQUIRE(true_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('f', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('f', char_type), radix_expr), ns));
     REQUIRE(false_exprt()==simplify_expr(
-      is_digit_with_radix(
-        from_integer('g', char_type),
-        from_integer(radix, int_type)), ns));
+      is_digit_with_radix(from_integer('g', char_type), radix_expr), ns));
   }
 }