From f9199a097a2c7d889b8ea95115e957294e8da450 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 26 May 2017 18:01:26 +0100
Subject: [PATCH 01/21] Make index_of precise diffblue/test-gen#77

Adding constraints to make sure the index_of primitive of the string
solver is precise.
Also add specific constraints for constant argument in indexOf to
improve performances in that case.
---
 .../string_constraint_generator_indexof.cpp   | 100 ++++++++++++++++--
 1 file changed, 89 insertions(+), 11 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index d799091a573..407bab2c5ba 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -73,12 +73,17 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 
 Function: string_constraint_generatort::add_axioms_for_index_of_string
 
-  Inputs: two string expressions and an integer expression
+  Inputs:
+    str - a string expression
+    substring - a string expression
+    from_index - an expression representing an index in strings
 
  Outputs: a integer expression
 
- Purpose: add axioms stating that the returned value is either -1 or greater
-          than from_index and the string beggining there has prefix substring
+ Purpose: add axioms stating that the returned value is an index greater than
+          from_index such that str at that index starts with substring and is
+          the first occurence of substring in str, or -1 if str does not contain
+          substring.
 
 \*******************************************************************/
 
@@ -92,20 +97,24 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => |str|-|substring|>=offset>=from_index
-  // a2 : !contains => offset=-1
-  // a3 : forall 0<=witness<|substring|.
-  //        contains => str[witness+offset]=substring[witness]
+  // a1 : contains => from_index <= offset <= |str|-|substring|
+  // a2 : !contains <=> offset=-1
+  // a3 : forall n:[0,|substring|[.
+  //        contains => str[n+offset]=substring[n]
+  // a4 : forall n:[from_index,offset[.
+  //        contains => (exists m:[0,|substring|[. str[m+n]!=substring[m]])
+  // a5:  forall n:[from_index,|str|-|substring|[.
+  //        !contains => (exists m:[0,|substring|[. str[m+n]!=substring[m])
 
   implies_exprt a1(
     contains,
     and_exprt(
-      str.axiom_for_is_longer_than(plus_exprt_with_overflow_check(
-        substring.length(), offset)),
-      binary_relation_exprt(offset, ID_ge, from_index)));
+      binary_relation_exprt(from_index, ID_le, offset),
+      binary_relation_exprt(
+        offset, ID_le, minus_exprt(str.length(), substring.length()))));
   axioms.push_back(a1);
 
-  implies_exprt a2(
+  equal_exprt a2(
     not_exprt(contains),
     equal_exprt(offset, from_integer(-1, index_type)));
   axioms.push_back(a2);
@@ -118,9 +127,78 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     equal_exprt(str[plus_exprt(qvar, offset)], substring[qvar]));
   axioms.push_back(a3);
 
+  if(!is_constant_string(substring))
+  {
+    // string_not contains_constraintt are formula of the form:
+    // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
+    string_not_contains_constraintt a4(
+      from_index,
+      offset,
+      contains,
+      from_integer(0, index_type),
+      substring.length(),
+      str,
+      substring);
+    axioms.push_back(a4);
+
+    string_not_contains_constraintt a5(
+      from_index,
+      minus_exprt(str.length(), substring.length()),
+      not_exprt(contains),
+      from_integer(0, index_type),
+      substring.length(),
+      str,
+      substring);
+    axioms.push_back(a5);
+  }
+  else
+  {
+    // Unfold the existential quantifier as a disjunction in case of a constant
+    // a4 && a5 <=> a6:
+    //  forall n:[from_index,|str|-|substring|].
+    //    !contains || n < offset =>
+    //       str[n]!=substring[0] || ... ||
+    //       str[n+|substring|-1]!=substring[|substring|-1]
+    symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
+    mp_integer sub_length;
+    assert(!to_integer(substring.length(), sub_length));
+    exprt::operandst disjuncts;
+    for(mp_integer offset=0; offset<sub_length; ++offset)
+    {
+      exprt expr_offset=from_integer(offset, index_type);
+      plus_exprt shifted(expr_offset, qvar2);
+      disjuncts.push_back(
+        not_exprt(equal_exprt(str[shifted], substring[expr_offset])));
+    }
+
+    or_exprt premise(
+      not_exprt(contains), binary_relation_exprt(qvar, ID_lt, offset));
+    minus_exprt length_diff(str.length(), substring.length());
+    string_constraintt a6(
+      qvar2,
+      from_index,
+      plus_exprt(from_integer(1, index_type), length_diff),
+      premise,
+      disjunction(disjuncts));
+    axioms.push_back(a6);
+  }
+
   return offset;
 }
 
+/*******************************************************************\
+
+Function: string_constraint_generatort::add_axioms_for_last_index_of_string
+
+  Inputs: two string expressions and an integer expression
+
+ Outputs: a integer expression
+
+ Purpose: add axioms stating that the returned value is either -1 or less
+          than from_index and the string beggining there has prefix substring
+
+\*******************************************************************/
+
 exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   const string_exprt &str,
   const string_exprt &substring,

From bc59d0c6acbd3e918f52741bac80398ab40bd7d6 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 31 May 2017 11:18:21 +0100
Subject: [PATCH 02/21] Making lastIndexOf precise diffblue/test-gen#77

---
 .../string_constraint_generator_indexof.cpp   | 57 +++++++++++++++----
 1 file changed, 47 insertions(+), 10 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 407bab2c5ba..c4400de5471 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -82,8 +82,8 @@ Function: string_constraint_generatort::add_axioms_for_index_of_string
 
  Purpose: add axioms stating that the returned value is an index greater than
           from_index such that str at that index starts with substring and is
-          the first occurence of substring in str, or -1 if str does not contain
-          substring.
+          the first occurence of substring in str after from_index,
+          or returned value is -1 if str does not contain substring.
 
 \*******************************************************************/
 
@@ -190,12 +190,17 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
 
 Function: string_constraint_generatort::add_axioms_for_last_index_of_string
 
-  Inputs: two string expressions and an integer expression
+  Inputs:
+    str - a string expression
+    substring - a string expression
+    from_index - an expression representing an index in strings
 
  Outputs: a integer expression
 
- Purpose: add axioms stating that the returned value is either -1 or less
-          than from_index and the string beggining there has prefix substring
+ Purpose: add axioms stating that the returned value is an index less than
+          from_index such that str at that index starts with substring and is
+          the last occurence of substring in str before from_index,
+          or the returned value is -1 if str does not contain substring.
 
 \*******************************************************************/
 
@@ -209,10 +214,16 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => |substring| >= length &&offset <= from_index
-  // a2 : !contains => offset=-1
-  // a3 : forall 0 <= witness<substring.length,
-  //        contains => str[witness+offset]=substring[witness]
+  // a1 : contains => |substring| >= length && offset <= from_index
+  // a2 : !contains <=> offset=-1
+  // a3 : forall n:[0, substring.length[,
+  //        contains => str[n+offset]=substring[n]
+  // a4 : forall n:[offset+1, min(from_index, |str| - |substring|)].
+  //        contains =>
+  //          (exists m:[0,|substring|[. str[m+n]!=substring[m]])
+  // a5:  forall n:[0, min(from_index, |str| - |substring|)].
+  //        !contains =>
+  //          (exists m:[0,|substring|[. str[m+n]!=substring[m])
 
   implies_exprt a1(
     contains,
@@ -222,7 +233,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
       binary_relation_exprt(offset, ID_le, from_index)));
   axioms.push_back(a1);
 
-  implies_exprt a2(
+  equal_exprt a2(
     not_exprt(contains),
     equal_exprt(offset, from_integer(-1, index_type)));
   axioms.push_back(a2);
@@ -232,6 +243,32 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   string_constraintt a3(qvar, substring.length(), contains, constr3);
   axioms.push_back(a3);
 
+  // end_index is min(from_index, |str| - |substring|)
+  minus_exprt length_diff(str.length(), substring.length());
+  if_exprt end_index(
+    binary_relation_exprt(from_index, ID_le, length_diff),
+    from_index,
+    length_diff);
+  string_not_contains_constraintt a4(
+    plus_exprt(offset, from_integer(1, index_type)),
+    from_index,
+    end_index,
+    from_integer(0, index_type),
+    substring.length(),
+    str,
+    substring);
+  axioms.push_back(a4);
+
+  string_not_contains_constraintt a5(
+    from_integer(0, index_type),
+    end_index,
+    not_exprt(contains),
+    from_integer(0, index_type),
+    substring.length(),
+    str,
+    substring);
+  axioms.push_back(a5);
+
   return offset;
 }
 

From 4f4df8e1a9d329dbfab02e5e20f97a7f029f58a8 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 31 May 2017 11:31:19 +0100
Subject: [PATCH 03/21] Optimize last_index_of for constant argument

---
 .../string_constraint_generator_indexof.cpp   | 70 ++++++++++++++-----
 1 file changed, 52 insertions(+), 18 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index c4400de5471..e0bb2ea1001 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -249,25 +249,59 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     binary_relation_exprt(from_index, ID_le, length_diff),
     from_index,
     length_diff);
-  string_not_contains_constraintt a4(
-    plus_exprt(offset, from_integer(1, index_type)),
-    from_index,
-    end_index,
-    from_integer(0, index_type),
-    substring.length(),
-    str,
-    substring);
-  axioms.push_back(a4);
 
-  string_not_contains_constraintt a5(
-    from_integer(0, index_type),
-    end_index,
-    not_exprt(contains),
-    from_integer(0, index_type),
-    substring.length(),
-    str,
-    substring);
-  axioms.push_back(a5);
+  if(!is_constant_string(substring))
+  {
+    string_not_contains_constraintt a4(
+      plus_exprt(offset, from_integer(1, index_type)),
+      from_index,
+      plus_exprt(end_index, from_integer(1, index_type)),
+      from_integer(0, index_type),
+      substring.length(),
+      str,
+      substring);
+    axioms.push_back(a4);
+
+    string_not_contains_constraintt a5(
+      from_integer(0, index_type),
+      plus_exprt(end_index, from_integer(1, index_type)),
+      not_exprt(contains),
+      from_integer(0, index_type),
+      substring.length(),
+      str,
+      substring);
+    axioms.push_back(a5);
+  }
+  else
+  {
+    // Unfold the existential quantifier as a disjunction in case of a constant
+    // a4 && a5 <=> a6:
+    //  forall n:[0, min(from_index,|str|-|substring|)].
+    //    !contains || n > offset =>
+    //       str[n]!=substring[0] || ... ||
+    //       str[n+|substring|-1]!=substring[|substring|-1]
+    symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
+    mp_integer sub_length;
+    assert(!to_integer(substring.length(), sub_length));
+    exprt::operandst disjuncts;
+    for(mp_integer offset=0; offset<sub_length; ++offset)
+    {
+      exprt expr_offset=from_integer(offset, index_type);
+      plus_exprt shifted(expr_offset, qvar2);
+      disjuncts.push_back(
+        not_exprt(equal_exprt(str[shifted], substring[expr_offset])));
+    }
+
+    or_exprt premise(
+      not_exprt(contains), binary_relation_exprt(qvar, ID_gt, offset));
+    string_constraintt a6(
+      qvar2,
+      from_index,
+      plus_exprt(from_integer(1, index_type), end_index),
+      premise,
+      disjunction(disjuncts));
+    axioms.push_back(a6);
+  }
 
   return offset;
 }

From 9b11653a8d431b3fbe2ff692ee5d0713aa164391 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 31 May 2017 11:22:07 +0100
Subject: [PATCH 04/21] Updating comments for index_of and last_index_of on
 characters

---
 .../string_constraint_generator_indexof.cpp   | 29 +++++++++++++++++--
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index e0bb2ea1001..6d2bd8e6bd5 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -13,12 +13,17 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 Function: string_constraint_generatort::add_axioms_for_index_of
 
-  Inputs: a string expression, a character expression and an integer expression
+  Inputs:
+    str - a string expression
+    c - an expression representing a character
+    from_index - an expression representing an index in the string
 
  Outputs: a integer expression
 
- Purpose: add axioms that the returned value is either -1 or greater than
-          from_index and the character at that position equals to c
+ Purpose: add axioms stating that the returned value is either:
+          -1 if the string does not contain c
+          an index greater than from_index such that the character of str at
+          that position equals c and is the first occurence after from_index.
 
 \*******************************************************************/
 
@@ -350,6 +355,24 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   }
 }
 
+/*******************************************************************\
+
+Function: string_constraint_generatort::add_axioms_for_last_index_of
+
+  Inputs:
+    str - a string expression
+    c - an expression representing a character
+    from_index - an expression representing an index in the string
+
+ Outputs: a integer expression
+
+ Purpose: add axioms stating that the returned value is either:
+          -1 if the string does not contain c
+          an index less than from_index such that the character of str at
+          that position equals c and is the last occurence before from_index.
+
+\*******************************************************************/
+
 exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const string_exprt &str, const exprt &c, const exprt &from_index)
 {

From bc3eedc52d9c82f5aab40937a91a18d5793f1cd7 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 5 Jun 2017 19:24:04 +0100
Subject: [PATCH 05/21] Replacing str and substring by haystack and needle

For clarity about the role of the arguments.
---
 .../refinement/string_constraint_generator.h  |  4 +-
 .../string_constraint_generator_indexof.cpp   | 42 +++++++++----------
 2 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 525f0fee3d7..c37b801e87e 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -198,8 +198,8 @@ class string_constraint_generatort
   // we add axioms stating that the returned value is either -1 or greater than
   // from_index and the string beggining there has prefix substring
   exprt add_axioms_for_index_of_string(
-    const string_exprt &str,
-    const string_exprt &substring,
+    const string_exprt &haystack,
+    const string_exprt &needle,
     const exprt &from_index);
 
   // Add axioms corresponding to the String.indexOf java functions
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 6d2bd8e6bd5..f3f03db455a 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -79,25 +79,25 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 Function: string_constraint_generatort::add_axioms_for_index_of_string
 
   Inputs:
-    str - a string expression
+    haystack - a string expression
     substring - a string expression
     from_index - an expression representing an index in strings
 
  Outputs: a integer expression
 
  Purpose: add axioms stating that the returned value is an index greater than
-          from_index such that str at that index starts with substring and is
-          the first occurence of substring in str after from_index,
-          or returned value is -1 if str does not contain substring.
+          from_index such that haystack at that index starts with needle and
+          is the first occurence of needle in haystack after from_index,
+          or returned value is -1 if haystack does not contain needle.
 
 \*******************************************************************/
 
 exprt string_constraint_generatort::add_axioms_for_index_of_string(
-  const string_exprt &str,
-  const string_exprt &substring,
+  const string_exprt &haystack,
+  const string_exprt &needle,
   const exprt &from_index)
 {
-  const typet &index_type=str.length().type();
+  const typet &index_type=haystack.length().type();
   symbol_exprt offset=fresh_exist_index("index_of", index_type);
   symbol_exprt contains=fresh_boolean("contains_substring");
 
@@ -116,7 +116,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     and_exprt(
       binary_relation_exprt(from_index, ID_le, offset),
       binary_relation_exprt(
-        offset, ID_le, minus_exprt(str.length(), substring.length()))));
+        offset, ID_le, minus_exprt(haystack.length(), needle.length()))));
   axioms.push_back(a1);
 
   equal_exprt a2(
@@ -127,12 +127,12 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   string_constraintt a3(
     qvar,
-    substring.length(),
+    needle.length(),
     contains,
-    equal_exprt(str[plus_exprt(qvar, offset)], substring[qvar]));
+    equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
   axioms.push_back(a3);
 
-  if(!is_constant_string(substring))
+  if(!is_constant_string(needle))
   {
     // string_not contains_constraintt are formula of the form:
     // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
@@ -141,19 +141,19 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
       offset,
       contains,
       from_integer(0, index_type),
-      substring.length(),
-      str,
-      substring);
+      needle.length(),
+      haystack,
+      needle);
     axioms.push_back(a4);
 
     string_not_contains_constraintt a5(
       from_index,
-      minus_exprt(str.length(), substring.length()),
+      minus_exprt(haystack.length(), needle.length()),
       not_exprt(contains),
       from_integer(0, index_type),
-      substring.length(),
-      str,
-      substring);
+      needle.length(),
+      haystack,
+      needle);
     axioms.push_back(a5);
   }
   else
@@ -166,19 +166,19 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     //       str[n+|substring|-1]!=substring[|substring|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
-    assert(!to_integer(substring.length(), sub_length));
+    assert(!to_integer(needle.length(), sub_length));
     exprt::operandst disjuncts;
     for(mp_integer offset=0; offset<sub_length; ++offset)
     {
       exprt expr_offset=from_integer(offset, index_type);
       plus_exprt shifted(expr_offset, qvar2);
       disjuncts.push_back(
-        not_exprt(equal_exprt(str[shifted], substring[expr_offset])));
+        not_exprt(equal_exprt(haystack[shifted], needle[expr_offset])));
     }
 
     or_exprt premise(
       not_exprt(contains), binary_relation_exprt(qvar, ID_lt, offset));
-    minus_exprt length_diff(str.length(), substring.length());
+    minus_exprt length_diff(haystack.length(), needle.length());
     string_constraintt a6(
       qvar2,
       from_index,

From 666bec08852e8d87d00571d592f66cc3fef611c6 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 5 Jun 2017 19:25:05 +0100
Subject: [PATCH 06/21] Removing comments about lastIndexOf being imprecise

The previous commits now make these functions precise.
---
 src/solvers/refinement/string_constraint_generator.h | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index c37b801e87e..fd19ee1452f 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -194,21 +194,15 @@ class string_constraint_generatort
     const exprt &from_index);
 
   // Add axioms corresponding to the String.indexOf:(String;I) java function
-  // TODO: the specifications are only partial:
-  // we add axioms stating that the returned value is either -1 or greater than
-  // from_index and the string beggining there has prefix substring
   exprt add_axioms_for_index_of_string(
     const string_exprt &haystack,
     const string_exprt &needle,
     const exprt &from_index);
 
   // Add axioms corresponding to the String.indexOf java functions
-  // TODO: the specifications are only partial for the ones that look for
-  // strings
   exprt add_axioms_for_index_of(const function_application_exprt &f);
 
   // Add axioms corresponding to the String.lastIndexOf:(String;I) java function
-  // TODO: the specifications are only partial
   exprt add_axioms_for_last_index_of_string(
     const string_exprt &str,
     const string_exprt &substring,
@@ -221,7 +215,6 @@ class string_constraint_generatort
     const exprt &from_index);
 
   // Add axioms corresponding to the String.lastIndexOf java functions
-  // TODO: the specifications is only partial
   exprt add_axioms_for_last_index_of(const function_application_exprt &f);
 
   // TODO: the specifications of these functions is only partial

From 1eb3263f1b24f540eb7b28c504381e5bfc1c1e43 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 5 Jun 2017 19:27:43 +0100
Subject: [PATCH 07/21] Making comments about the output more precise

---
 .../refinement/string_constraint_generator_indexof.cpp      | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index f3f03db455a..799f15a3af5 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -83,7 +83,8 @@ Function: string_constraint_generatort::add_axioms_for_index_of_string
     substring - a string expression
     from_index - an expression representing an index in strings
 
- Outputs: a integer expression
+ Outputs: an integer expression representing the first index of needle in
+          haystack after from_index, or -1 if there is none
 
  Purpose: add axioms stating that the returned value is an index greater than
           from_index such that haystack at that index starts with needle and
@@ -200,7 +201,8 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of_string
     substring - a string expression
     from_index - an expression representing an index in strings
 
- Outputs: a integer expression
+ Outputs: an integer expression representing the last index of needle in
+          haystack after from_index, or -1 if there is none
 
  Purpose: add axioms stating that the returned value is an index less than
           from_index such that str at that index starts with substring and is

From 68cdc6fd117f06467190dbba63dde6bba4cd4cb1 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 5 Jun 2017 19:29:38 +0100
Subject: [PATCH 08/21] Renaming str and substring to haystack and needle

---
 .../refinement/string_constraint_generator.h  |  4 +--
 .../string_constraint_generator_indexof.cpp   | 34 +++++++++----------
 2 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index fd19ee1452f..94234b810de 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -204,8 +204,8 @@ class string_constraint_generatort
 
   // Add axioms corresponding to the String.lastIndexOf:(String;I) java function
   exprt add_axioms_for_last_index_of_string(
-    const string_exprt &str,
-    const string_exprt &substring,
+    const string_exprt &haystack,
+    const string_exprt &needle,
     const exprt &from_index);
 
   // Add axioms corresponding to the String.lastIndexOf:(CI) java function
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 799f15a3af5..053f11f60a6 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -212,11 +212,11 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of_string
 \*******************************************************************/
 
 exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
-  const string_exprt &str,
-  const string_exprt &substring,
+  const string_exprt &haystack,
+  const string_exprt &needle,
   const exprt &from_index)
 {
-  const typet &index_type=str.length().type();
+  const typet &index_type=haystack.length().type();
   symbol_exprt offset=fresh_exist_index("index_of", index_type);
   symbol_exprt contains=fresh_boolean("contains_substring");
 
@@ -235,8 +235,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   implies_exprt a1(
     contains,
     and_exprt(
-      str.axiom_for_is_longer_than(
-        plus_exprt_with_overflow_check(substring.length(), offset)),
+      haystack.axiom_for_is_longer_than(
+        plus_exprt_with_overflow_check(needle.length(), offset)),
       binary_relation_exprt(offset, ID_le, from_index)));
   axioms.push_back(a1);
 
@@ -246,27 +246,27 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   axioms.push_back(a2);
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
-  equal_exprt constr3(str[plus_exprt(qvar, offset)], substring[qvar]);
-  string_constraintt a3(qvar, substring.length(), contains, constr3);
+  equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
+  string_constraintt a3(qvar, needle.length(), contains, constr3);
   axioms.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
-  minus_exprt length_diff(str.length(), substring.length());
+  minus_exprt length_diff(haystack.length(), needle.length());
   if_exprt end_index(
     binary_relation_exprt(from_index, ID_le, length_diff),
     from_index,
     length_diff);
 
-  if(!is_constant_string(substring))
+  if(!is_constant_string(needle))
   {
     string_not_contains_constraintt a4(
       plus_exprt(offset, from_integer(1, index_type)),
       from_index,
       plus_exprt(end_index, from_integer(1, index_type)),
       from_integer(0, index_type),
-      substring.length(),
-      str,
-      substring);
+      needle.length(),
+      haystack,
+      needle);
     axioms.push_back(a4);
 
     string_not_contains_constraintt a5(
@@ -274,9 +274,9 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
       plus_exprt(end_index, from_integer(1, index_type)),
       not_exprt(contains),
       from_integer(0, index_type),
-      substring.length(),
-      str,
-      substring);
+      needle.length(),
+      haystack,
+      needle);
     axioms.push_back(a5);
   }
   else
@@ -289,14 +289,14 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     //       str[n+|substring|-1]!=substring[|substring|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
-    assert(!to_integer(substring.length(), sub_length));
+    assert(!to_integer(needle.length(), sub_length));
     exprt::operandst disjuncts;
     for(mp_integer offset=0; offset<sub_length; ++offset)
     {
       exprt expr_offset=from_integer(offset, index_type);
       plus_exprt shifted(expr_offset, qvar2);
       disjuncts.push_back(
-        not_exprt(equal_exprt(str[shifted], substring[expr_offset])));
+        not_exprt(equal_exprt(haystack[shifted], needle[expr_offset])));
     }
 
     or_exprt premise(

From 2d16c2cf96e916c34397b0b64eca72a037acfaca Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 5 Jun 2017 19:33:12 +0100
Subject: [PATCH 09/21] Correct comments and axioms in lastIndexOf

This new version should be clearer and the added axioms match the
comments.
---
 .../refinement/string_constraint_generator_indexof.cpp      | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 053f11f60a6..4e2914c003f 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -221,7 +221,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => |substring| >= length && offset <= from_index
+  // a1 : contains => offset <= from_index && offset <= |haystack| - |needle|
   // a2 : !contains <=> offset=-1
   // a3 : forall n:[0, substring.length[,
   //        contains => str[n+offset]=substring[n]
@@ -235,8 +235,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   implies_exprt a1(
     contains,
     and_exprt(
-      haystack.axiom_for_is_longer_than(
-        plus_exprt_with_overflow_check(needle.length(), offset)),
+      binary_relation_exprt(
+        offset, ID_le, minus_exprt(haystack.length(), needle.length())),
       binary_relation_exprt(offset, ID_le, from_index)));
   axioms.push_back(a1);
 

From f3f5a19b225eec8ee9bd7a50291bca83a5176f98 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 5 Jun 2017 19:37:48 +0100
Subject: [PATCH 10/21] Replacing str and substring by haystack and needle in
 the comments

This is to match the names of the variables.
---
 .../string_constraint_generator_indexof.cpp   | 34 +++++++++----------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 4e2914c003f..4449f7cafc6 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -103,14 +103,14 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => from_index <= offset <= |str|-|substring|
+  // a1 : contains => from_index <= offset <= |haystack|-|needle|
   // a2 : !contains <=> offset=-1
   // a3 : forall n:[0,|substring|[.
-  //        contains => str[n+offset]=substring[n]
+  //        contains => haystack[n+offset]=needle[n]
   // a4 : forall n:[from_index,offset[.
-  //        contains => (exists m:[0,|substring|[. str[m+n]!=substring[m]])
-  // a5:  forall n:[from_index,|str|-|substring|[.
-  //        !contains => (exists m:[0,|substring|[. str[m+n]!=substring[m])
+  //        contains => (exists m:[0,|needle|[. haystack[m+n]!=needle[m]])
+  // a5:  forall n:[from_index,|haystack|-|needle|[.
+  //        !contains => (exists m:[0,|needle|[. haystack[m+n]!=needle[m])
 
   implies_exprt a1(
     contains,
@@ -161,10 +161,10 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   {
     // Unfold the existential quantifier as a disjunction in case of a constant
     // a4 && a5 <=> a6:
-    //  forall n:[from_index,|str|-|substring|].
+    //  forall n:[from_index,|haystack|-|needle|].
     //    !contains || n < offset =>
-    //       str[n]!=substring[0] || ... ||
-    //       str[n+|substring|-1]!=substring[|substring|-1]
+    //       haystack[n]!=needle[0] || ... ||
+    //       haystack[n+|needle|-1]!=needle[|needle|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));
@@ -223,14 +223,14 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   // We add axioms:
   // a1 : contains => offset <= from_index && offset <= |haystack| - |needle|
   // a2 : !contains <=> offset=-1
-  // a3 : forall n:[0, substring.length[,
-  //        contains => str[n+offset]=substring[n]
-  // a4 : forall n:[offset+1, min(from_index, |str| - |substring|)].
+  // a3 : forall n:[0, needle.length[,
+  //        contains => haystack[n+offset]=needle[n]
+  // a4 : forall n:[offset+1, min(from_index, |haystack| - |needle|)].
   //        contains =>
-  //          (exists m:[0,|substring|[. str[m+n]!=substring[m]])
-  // a5:  forall n:[0, min(from_index, |str| - |substring|)].
+  //          (exists m:[0,|substring|[. haystack[m+n]!=needle[m]])
+  // a5:  forall n:[0, min(from_index, |haystack| - |needle|)].
   //        !contains =>
-  //          (exists m:[0,|substring|[. str[m+n]!=substring[m])
+  //          (exists m:[0,|substring|[. haystack[m+n]!=needle[m])
 
   implies_exprt a1(
     contains,
@@ -283,10 +283,10 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   {
     // Unfold the existential quantifier as a disjunction in case of a constant
     // a4 && a5 <=> a6:
-    //  forall n:[0, min(from_index,|str|-|substring|)].
+    //  forall n:[0, min(from_index,|haystack|-|needle|)].
     //    !contains || n > offset =>
-    //       str[n]!=substring[0] || ... ||
-    //       str[n+|substring|-1]!=substring[|substring|-1]
+    //       haystack[n]!=needle[0] || ... ||
+    //       haystack[n+|substring|-1]!=needle[|substring|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));

From a4ab7db7b09b0b498731fd7a4577a892993f8a67 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 09:37:18 +0100
Subject: [PATCH 11/21] Updating comments for functions adding axioms for
 index_of

---
 .../string_constraint_generator_indexof.cpp   | 37 +++++++++----------
 1 file changed, 18 insertions(+), 19 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 4449f7cafc6..1676699086a 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -20,10 +20,9 @@ Function: string_constraint_generatort::add_axioms_for_index_of
 
  Outputs: a integer expression
 
- Purpose: add axioms stating that the returned value is either:
-          -1 if the string does not contain c
-          an index greater than from_index such that the character of str at
-          that position equals c and is the first occurence after from_index.
+ Purpose: Add axioms stating that the returned value is the index within
+          str of the first occurence of c starting the search at from_index,
+          or -1 if no such character occurs at or after position from_index.
 
 \*******************************************************************/
 
@@ -80,16 +79,16 @@ Function: string_constraint_generatort::add_axioms_for_index_of_string
 
   Inputs:
     haystack - a string expression
-    substring - a string expression
+    needle - a string expression
     from_index - an expression representing an index in strings
 
  Outputs: an integer expression representing the first index of needle in
           haystack after from_index, or -1 if there is none
 
- Purpose: add axioms stating that the returned value is an index greater than
-          from_index such that haystack at that index starts with needle and
-          is the first occurence of needle in haystack after from_index,
-          or returned value is -1 if haystack does not contain needle.
+ Purpose: Add axioms stating that the returned value is the index within
+          haystack of the first occurence of needle starting the search at
+          from_index, or -1 if needle does not occur at or after position
+          from_index.
 
 \*******************************************************************/
 
@@ -197,17 +196,17 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
 Function: string_constraint_generatort::add_axioms_for_last_index_of_string
 
   Inputs:
-    str - a string expression
-    substring - a string expression
+    haystack - a string expression
+    needle - a string expression
     from_index - an expression representing an index in strings
 
  Outputs: an integer expression representing the last index of needle in
           haystack after from_index, or -1 if there is none
 
- Purpose: add axioms stating that the returned value is an index less than
-          from_index such that str at that index starts with substring and is
-          the last occurence of substring in str before from_index,
-          or the returned value is -1 if str does not contain substring.
+ Purpose: Add axioms stating that the returned value is the index within
+          haystack of the last occurence of needle starting the search
+          backward at from_index (ie the index is smaller or equal to
+          from_index), or -1 if needle does not occur before from_index.
 
 \*******************************************************************/
 
@@ -368,10 +367,10 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of
 
  Outputs: a integer expression
 
- Purpose: add axioms stating that the returned value is either:
-          -1 if the string does not contain c
-          an index less than from_index such that the character of str at
-          that position equals c and is the last occurence before from_index.
+ Purpose: Add axioms stating that the returned value is the index within
+          str of the last occurence of c starting the search backward at
+          from_index, or -1 if no such character occurs at or before
+          position from_index.
 
 \*******************************************************************/
 

From 1eb7d748e6de2145e65f5674ef3a2c349b5d53b7 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 09:59:00 +0100
Subject: [PATCH 12/21] Uniformising mathematical notations in comments

Use spaces around comparison operators (=, <=, != etc...)
Use ==> to denote implication.
n:[lb, ub[ for interval between lb (inclusive) and ub (exclusive).
|str| for length of string str.
---
 .../string_constraint_generator_indexof.cpp   | 50 +++++++++----------
 1 file changed, 25 insertions(+), 25 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 1676699086a..3d8b1660451 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -34,11 +34,11 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   symbol_exprt contains=fresh_boolean("contains_in_index_of");
 
   // We add axioms:
-  // a1 : -1 <= index<|str|
+  // a1 : -1 <= index < |str|
   // a2 : !contains <=> index=-1
-  // a3 : contains => from_index<=index&&str[index]=c
-  // a4 : forall n, from_index<=n<index. contains => str[n]!=c
-  // a5 : forall m, from_index<=n<|str|. !contains => str[m]!=c
+  // a3 : contains ==> from_index <= index && str[index] = c
+  // a4 : forall n, n:[from_index,index[. contains ==> str[n] != c
+  // a5 : forall m, n:[from_index,|str|[. !contains ==> str[m] != c
 
   exprt minus1=from_integer(-1, index_type);
   and_exprt a1(
@@ -102,14 +102,14 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => from_index <= offset <= |haystack|-|needle|
+  // a1 : contains ==> from_index <= offset <= |haystack|-|needle|
   // a2 : !contains <=> offset=-1
   // a3 : forall n:[0,|substring|[.
-  //        contains => haystack[n+offset]=needle[n]
+  //        contains ==> haystack[n+offset]=needle[n]
   // a4 : forall n:[from_index,offset[.
-  //        contains => (exists m:[0,|needle|[. haystack[m+n]!=needle[m]])
+  //        contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]])
   // a5:  forall n:[from_index,|haystack|-|needle|[.
-  //        !contains => (exists m:[0,|needle|[. haystack[m+n]!=needle[m])
+  //        !contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m])
 
   implies_exprt a1(
     contains,
@@ -161,9 +161,9 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     // Unfold the existential quantifier as a disjunction in case of a constant
     // a4 && a5 <=> a6:
     //  forall n:[from_index,|haystack|-|needle|].
-    //    !contains || n < offset =>
-    //       haystack[n]!=needle[0] || ... ||
-    //       haystack[n+|needle|-1]!=needle[|needle|-1]
+    //    !contains || n < offset ==>
+    //       haystack[n] != needle[0] || ... ||
+    //       haystack[n+|needle|-1] != needle[|needle|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));
@@ -220,16 +220,16 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => offset <= from_index && offset <= |haystack| - |needle|
-  // a2 : !contains <=> offset=-1
+  // a1 : contains ==> offset <= from_index && offset <= |haystack| - |needle|
+  // a2 : !contains <=> offset = -1
   // a3 : forall n:[0, needle.length[,
-  //        contains => haystack[n+offset]=needle[n]
+  //        contains ==> haystack[n+offset] = needle[n]
   // a4 : forall n:[offset+1, min(from_index, |haystack| - |needle|)].
-  //        contains =>
-  //          (exists m:[0,|substring|[. haystack[m+n]!=needle[m]])
+  //        contains ==>
+  //          (exists m:[0,|substring|[. haystack[m+n] != needle[m]])
   // a5:  forall n:[0, min(from_index, |haystack| - |needle|)].
-  //        !contains =>
-  //          (exists m:[0,|substring|[. haystack[m+n]!=needle[m])
+  //        !contains ==>
+  //          (exists m:[0,|substring|[. haystack[m+n] != needle[m])
 
   implies_exprt a1(
     contains,
@@ -283,9 +283,9 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     // Unfold the existential quantifier as a disjunction in case of a constant
     // a4 && a5 <=> a6:
     //  forall n:[0, min(from_index,|haystack|-|needle|)].
-    //    !contains || n > offset =>
-    //       haystack[n]!=needle[0] || ... ||
-    //       haystack[n+|substring|-1]!=needle[|substring|-1]
+    //    !contains || n > offset ==>
+    //       haystack[n] != needle[0] || ... ||
+    //       haystack[n+|substring|-1] != needle[|substring|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));
@@ -384,10 +384,10 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
 
   // We add axioms:
   // a1 : -1 <= i <= from_index
-  // a2 : (i=-1 <=> !contains)
-  // a3 : (contains => i <= from_index &&s[i]=c)
-  // a4 : forall n. i+1 <= n < from_index +1 &&contains => s[n]!=c
-  // a5 : forall m. 0 <= m < from_index +1 &&!contains => s[m]!=c
+  // a2 : i = -1 <=> !contains
+  // a3 : contains ==> (i <= from_index && s[i] = c)
+  // a4 : forall n:[i+1, from_index+1[ && contains ==> s[n] != c
+  // a5 : forall m:[0, from_index+1[ && !contains ==> s[m] != c
 
   exprt index1=from_integer(1, index_type);
   exprt minus1=from_integer(-1, index_type);

From 069da51617bb5192891d99c5969aeca48e2ba963 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 10:10:18 +0100
Subject: [PATCH 13/21] Typo in comment

---
 src/solvers/refinement/string_constraint_generator_indexof.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 3d8b1660451..7e9622b1aec 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -134,7 +134,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
 
   if(!is_constant_string(needle))
   {
-    // string_not contains_constraintt are formula of the form:
+    // string_not contains_constraintt are formulas of the form:
     // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
     string_not_contains_constraintt a4(
       from_index,

From 7edfe0d2d756bacab5d3365d6c61a42ed355c709 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 10:29:57 +0100
Subject: [PATCH 14/21] Typo in comment

---
 src/solvers/refinement/string_constraint_generator_indexof.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 7e9622b1aec..3e952de588b 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -104,7 +104,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   // We add axioms:
   // a1 : contains ==> from_index <= offset <= |haystack|-|needle|
   // a2 : !contains <=> offset=-1
-  // a3 : forall n:[0,|substring|[.
+  // a3 : forall n:[0,|needle|[.
   //        contains ==> haystack[n+offset]=needle[n]
   // a4 : forall n:[from_index,offset[.
   //        contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]])

From 3e9668a71e5e9a3ddd1043b6a9346df7146c2f64 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 10:35:50 +0100
Subject: [PATCH 15/21] Correcting a mistake, universal variable was used in
 non-quantified formula

---
 src/solvers/refinement/string_constraint_generator_indexof.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 3e952de588b..e70a96f9a4d 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -177,7 +177,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     }
 
     or_exprt premise(
-      not_exprt(contains), binary_relation_exprt(qvar, ID_lt, offset));
+      not_exprt(contains), binary_relation_exprt(qvar2, ID_lt, offset));
     minus_exprt length_diff(haystack.length(), needle.length());
     string_constraintt a6(
       qvar2,

From b06476c47e5e521ef706883d808f5185758f7bb4 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 10:39:59 +0100
Subject: [PATCH 16/21] Correcting indentation in the comments

---
 .../refinement/string_constraint_generator_indexof.cpp    | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index e70a96f9a4d..5ae9d2c66b6 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -162,8 +162,8 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     // a4 && a5 <=> a6:
     //  forall n:[from_index,|haystack|-|needle|].
     //    !contains || n < offset ==>
-    //       haystack[n] != needle[0] || ... ||
-    //       haystack[n+|needle|-1] != needle[|needle|-1]
+    //      haystack[n] != needle[0] || ... ||
+    //      haystack[n+|needle|-1] != needle[|needle|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));
@@ -284,8 +284,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     // a4 && a5 <=> a6:
     //  forall n:[0, min(from_index,|haystack|-|needle|)].
     //    !contains || n > offset ==>
-    //       haystack[n] != needle[0] || ... ||
-    //       haystack[n+|substring|-1] != needle[|substring|-1]
+    //      haystack[n] != needle[0] || ... ||
+    //      haystack[n+|substring|-1] != needle[|substring|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));

From af98378f845ab196b4a02c62c9cda4827ce8638e Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 12:34:52 +0100
Subject: [PATCH 17/21] Correcting misuse of univ variable qvar instead of
 qvar2

---
 src/solvers/refinement/string_constraint_generator_indexof.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 5ae9d2c66b6..11bc7176451 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -299,7 +299,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     }
 
     or_exprt premise(
-      not_exprt(contains), binary_relation_exprt(qvar, ID_gt, offset));
+      not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));
     string_constraintt a6(
       qvar2,
       from_index,

From 80dff96f90934cdf48a2163a80c9f3a290328f91 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 12:40:37 +0100
Subject: [PATCH 18/21] Correcting lower bound in axiom added for last_index_of

---
 .../refinement/string_constraint_generator_indexof.cpp        | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 11bc7176451..8da9d0b557e 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -285,7 +285,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     //  forall n:[0, min(from_index,|haystack|-|needle|)].
     //    !contains || n > offset ==>
     //      haystack[n] != needle[0] || ... ||
-    //      haystack[n+|substring|-1] != needle[|substring|-1]
+    //      haystack[n+|needle|-1] != needle[|needle|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
     assert(!to_integer(needle.length(), sub_length));
@@ -302,7 +302,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
       not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));
     string_constraintt a6(
       qvar2,
-      from_index,
+      from_integer(0, index_type),
       plus_exprt(from_integer(1, index_type), end_index),
       premise,
       disjunction(disjuncts));

From d4a9b2a5b8b5ed8195b03f720c30b6b5439b8093 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 12:45:06 +0100
Subject: [PATCH 19/21] More comments on the output of last_index_of functions

---
 .../refinement/string_constraint_generator_indexof.cpp       | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 8da9d0b557e..26060383558 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -201,7 +201,7 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of_string
     from_index - an expression representing an index in strings
 
  Outputs: an integer expression representing the last index of needle in
-          haystack after from_index, or -1 if there is none
+          haystack before or at from_index, or -1 if there is none
 
  Purpose: Add axioms stating that the returned value is the index within
           haystack of the last occurence of needle starting the search
@@ -365,7 +365,8 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of
     c - an expression representing a character
     from_index - an expression representing an index in the string
 
- Outputs: a integer expression
+ Outputs: an integer expression representing the last index of c in
+          str before or at from_index, or -1 if there is none
 
  Purpose: Add axioms stating that the returned value is the index within
           str of the last occurence of c starting the search backward at

From 94f99b5d54d37e3cd680f72d245bb13d23882f07 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 6 Jun 2017 12:56:49 +0100
Subject: [PATCH 20/21] Adding forgotten precondition in not_contains
 constraint

---
 src/solvers/refinement/string_constraint_generator_indexof.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 26060383558..9386639e594 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -260,8 +260,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   {
     string_not_contains_constraintt a4(
       plus_exprt(offset, from_integer(1, index_type)),
-      from_index,
       plus_exprt(end_index, from_integer(1, index_type)),
+      contains,
       from_integer(0, index_type),
       needle.length(),
       haystack,

From cf5b5d3747a5f790e9a0fb75ea9a995a21d8a77d Mon Sep 17 00:00:00 2001
From: Joel Allred <joel.allred@diffblue.com>
Date: Tue, 6 Jun 2017 17:33:05 +0100
Subject: [PATCH 21/21] Update regressions tests for indexOf and lastIndexOf

---
 .../java_index_of/test.desc                    |   3 +--
 .../java_index_of/test_index_of.class          | Bin 631 -> 690 bytes
 .../java_index_of/test_index_of.java           |  17 ++++++++++-------
 .../java_last_index_of/test.desc               |   8 ++++----
 .../test_last_index_of.class                   | Bin 647 -> 671 bytes
 .../java_last_index_of/test_last_index_of.java |  15 ++++++++-------
 6 files changed, 23 insertions(+), 20 deletions(-)

diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc
index 6033af25d1b..e0e7de66561 100644
--- a/regression/strings-smoke-tests/java_index_of/test.desc
+++ b/regression/strings-smoke-tests/java_index_of/test.desc
@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 test_index_of.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-Issue: cbmc/test-gen#77
diff --git a/regression/strings-smoke-tests/java_index_of/test_index_of.class b/regression/strings-smoke-tests/java_index_of/test_index_of.class
index 1acb3335d57d4664c88fb229efaf15666076d900..8a989bdc95c15947a16aef455041837610fc8abd 100644
GIT binary patch
delta 407
zcmYk1&n^Q|6vlt|&fK{((?L7csz0TwMF){c*=bng0mKTgA?Xv4G<MxsTDOumAz|+c
zyonvojA-QEeCOQnd^z8DKi#3(fB$-Z1==JbIVwK$J_|mJAxl&P0+uZ+A(o1z7P3m+
zvew(XP>tT*Zf%+wg>!s$t<V`<URfFuP1YkKrg|Sc-bTbGt^1t1=>}o}Dql%w(m5z(
zg<xJ@RjEp<Nyex_Dx@IjWu%fQ@kDxy#>lJ_>yy|yjoq_kYlP_}+kyw~5U)?Z>OPQr
z!Jd!t-%_eeq2%g+WNM-_lRCciMiO~)teE*?7EmUnC8-Z3aZwZ{^tTYkGW&a#Brb}$
mG|AS^@<JgFMudH=`-tm2;SHJ-yT3oBD-Ak2N`GF?#&bXYvMS~P

delta 347
zcmYL^OHRWu5QaY|aqOf9(iGZ4Tl(OsB7}s>5((CD0btjjfISjth}d<*k~OW=N+7|W
zQ*aA*6_ZF5*_yG(|9rn^qJM(Zuf^L3FyJsIre>*IHe<GEL|B@JR!m6EupQH;W9VjQ
zcdD0VCyf<W75?RLr0|9#L(j3puA_v@zK_E_$36#774`6F1q~{x=WlZIQAoGMHMzAU
zE6KV)N4@4k5{Y3^R78}Q(px-fhED2TrT%sQXhv{8L61qA!84_I!kanfGpBe3rHbZW
z*wPltGU9J#kcd<y4z-|dsK{1QUtbyx3Uer@c1ASD1TO^s6#Y;B`(F;yc<v&fVxusw
F{sR4tA?g4C

diff --git a/regression/strings-smoke-tests/java_index_of/test_index_of.java b/regression/strings-smoke-tests/java_index_of/test_index_of.java
index 270267196c5..3568dab9696 100644
--- a/regression/strings-smoke-tests/java_index_of/test_index_of.java
+++ b/regression/strings-smoke-tests/java_index_of/test_index_of.java
@@ -1,10 +1,13 @@
 public class test_index_of
 {
-   public static void main(/*String[] argv*/)
-   {
-      String s = "Abc";
-      String bc = "bc";
-      int i = s.indexOf(bc);
-      assert(i == 1);
-   }
+    public static void main(/*String[] argv*/)
+    {
+        String s = "Abc";
+        String bc = "bc";
+        String ab = "ab";
+        int i = s.indexOf(bc);
+        int j = s.indexOf(ab);
+        assert(i == 1);
+        assert(j == -1);
+    }
 }
diff --git a/regression/strings-smoke-tests/java_last_index_of/test.desc b/regression/strings-smoke-tests/java_last_index_of/test.desc
index 5ee1604e846..381078254cd 100644
--- a/regression/strings-smoke-tests/java_last_index_of/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of/test.desc
@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 test_last_index_of.class
 --refine-strings
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
 --
-Issue: diffblue/test-gen#77
diff --git a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class
index 4455da4d17990ad4ba7072f2330d39bebd49531c..26f5ec3a7c3c8bf37de19628b3e62341f18bc2e4 100644
GIT binary patch
delta 101
zcmZo?ozJ@A0V8J-0}}%?0|SHc<d=-{-kTU$XE6xKu*_%R-p#-kxt)Q1|3;uB6N3Pd
wlwx25lB_`GY(U7)z{9}7AkV<bV8p=1AOw`*WnlWpAkWSq3`C4VldYM20Fo*WH2?qr

delta 71
zcmbQw+RnP+0V8J=0}}%?0|SG?<d=-{lckxsG{qQLfqYh=C>s#6Gw?8QFvv4-G6(@h
Uc^DY~G03ws2m=x0<X|Qr0D@)+-~a#s

diff --git a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java
index 8b3a0904d5b..59b9f5ab36d 100644
--- a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java
+++ b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java
@@ -1,10 +1,11 @@
 public class test_last_index_of
 {
-   public static void main(/*String[] argv*/)
-   {
-      String s = "abcab";
-      String ab = "ab";
-      int i = s.lastIndexOf(ab);
-      assert(i == 3);
-   }
+    public static void main(/*String[] argv*/)
+    {
+        String s = "abcab";
+        String ab = "ab";
+        int i = s.lastIndexOf(ab);
+        assert(i == 3);
+        assert(i == 1);
+    }
 }