diff --git a/regression/strings-smoke-tests/java_last_index_of2/test.desc b/regression/strings-smoke-tests/java_last_index_of2/test.desc
new file mode 100644
index 00000000000..5348cbe7fce
--- /dev/null
+++ b/regression/strings-smoke-tests/java_last_index_of2/test.desc
@@ -0,0 +1,7 @@
+CORE
+test_last_index_of2.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.class b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.class
new file mode 100644
index 00000000000..9c82a704075
Binary files /dev/null and b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.class differ
diff --git a/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java
new file mode 100644
index 00000000000..f533835fda4
--- /dev/null
+++ b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java
@@ -0,0 +1,8 @@
+public class test_last_index_of2
+{
+   public static void main(String[] args)
+   {
+      String letters = "automatictestcasegenerationatdiffblue";
+      assert(letters.lastIndexOf("diffblue", 25)==-1);
+   }
+}
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 2e3e6424c36..677262092e1 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -193,20 +193,22 @@ 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|
+  // a1 : contains ==> -1 <= offset && offset <= from_index
+  //                   && offset <= |haystack| - |needle|
   // a2 : !contains <=> offset = -1
-  // a3 : forall n:[0, needle.length[,
+  // a3 : forall n:[0, |needle|[,
   //        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]])
+  //          (exists m:[0,|needle|[. haystack[m+n] != needle[m]])
   // a5:  forall n:[0, min(from_index, |haystack| - |needle|)].
   //        !contains ==>
-  //          (exists m:[0,|substring|[. haystack[m+n] != needle[m])
+  //          (exists m:[0,|needle|[. haystack[m+n] != needle[m])
 
   implies_exprt a1(
     contains,
     and_exprt(
+      binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
       binary_relation_exprt(
         offset, ID_le, minus_exprt(haystack.length(), needle.length())),
       binary_relation_exprt(offset, ID_le, from_index)));
@@ -255,8 +257,8 @@ 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 ==>
+    //  forall n:[0, min(from_index, |haystack| - |needle|)].
+    //    !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);
@@ -273,6 +275,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
 
     or_exprt premise(
       not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));
+
     string_constraintt a6(
       qvar2,
       from_integer(0, index_type),