diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.class b/regression/jbmc-strings/StringLastIndexOf/Test.class
new file mode 100644
index 00000000000..609cc4f3348
Binary files /dev/null and b/regression/jbmc-strings/StringLastIndexOf/Test.class differ
diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.java b/regression/jbmc-strings/StringLastIndexOf/Test.java
new file mode 100644
index 00000000000..38436b885bf
--- /dev/null
+++ b/regression/jbmc-strings/StringLastIndexOf/Test.java
@@ -0,0 +1,24 @@
+public class Test {
+    int fromIndex;
+
+    public void check(String input_String1, String input_String2, int i) {
+        if(input_String1 != null && input_String2 != null) {
+            if (i == 0) {
+                // The last occurrence of the empty string "" is considered to
+                // occur at the index value this.length()
+                int lio = input_String1.lastIndexOf(input_String2);
+                if (input_String2.length() == 0)
+                    assert lio == input_String1.length();
+            } else if (i == 1) {
+                // Contradiction with the previous condition (should fail).
+                assert "foo".lastIndexOf("") != 3;
+            } else if (i == 2 && input_String2.length() > 0) {
+                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                if (input_String2.length() == 0)
+                    assert lio == fromIndex;
+            } else if (i == 3) {
+                assert "foo".lastIndexOf("", 2) != 2;
+            }
+        }
+    }
+}
diff --git a/regression/jbmc-strings/StringLastIndexOf/test.desc b/regression/jbmc-strings/StringLastIndexOf/test.desc
new file mode 100644
index 00000000000..4f1852669c0
--- /dev/null
+++ b/regression/jbmc-strings/StringLastIndexOf/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check --refine-strings --string-max-length 100
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 11 .* SUCCESS$
+assertion at file Test.java line 14 .* FAILURE$
+assertion at file Test.java line 18 .* SUCCESS$
+assertion at file Test.java line 20 .* FAILURE$
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index edf532751d1..11067029b5a 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -80,6 +80,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 /// `haystack` of the first occurrence of `needle` starting the search at
 /// `from_index`, or `-1` if needle does not occur at or after position
 /// `from_index`.
+/// If needle is an empty string then the result is `from_index`.
 ///
 /// These axioms are:
 ///   1. \f$ contains \Rightarrow {\tt from\_index} \le \tt{index}
@@ -93,6 +94,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 ///   5. \f$ \forall n \in [{\tt from\_index},|{\tt haystack}|-|{\tt needle}|]
 ///          .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|)
 ///          .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$
+///   6. \f$ |{\tt needle}| = 0 \Rightarrow \tt{index} = from_index \f$
 /// \param haystack: an array of character expression
 /// \param needle: an array of character expression
 /// \param from_index: an integer expression
@@ -152,6 +154,11 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     needle);
   axioms.push_back(a5);
 
+  const implies_exprt a6(
+    equal_exprt(needle.length(), from_integer(0, index_type)),
+    equal_exprt(offset, from_index));
+  axioms.push_back(a6);
+
   return offset;
 }
 
@@ -159,6 +166,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
 /// the last occurrence 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.
+/// If `needle` is the empty string, the result is `from_index`.
 ///
 /// These axioms are:
 ///   1. \f$ contains \Rightarrow -1 \le {\tt index}
@@ -178,6 +186,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
 ///          .\ \lnot contains \Rightarrow
 ///          (\exists m \in [0,|{\tt needle}|)
 ///          .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$
+///   6. \f$ |{\tt needle}| = 0 \Rightarrow index = from_index \f$
 /// \param haystack: an array of characters expression
 /// \param needle: an array of characters expression
 /// \param from_index: integer expression
@@ -238,6 +247,11 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     needle);
   axioms.push_back(a5);
 
+  const implies_exprt a6(
+    equal_exprt(needle.length(), from_integer(0, index_type)),
+    equal_exprt(offset, from_index));
+  axioms.push_back(a6);
+
   return offset;
 }
 
@@ -295,13 +309,16 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 /// \todo Change argument names to match add_axioms_for_last_index_of_string
 ///
 /// These axioms are :
-///   1. \f$ -1 \le {\tt index} \le {\tt from\_index} \f$
+///   1. \f$ -1 \le {\tt index} \le {\tt from\_index}
+///          \land {\tt index} < |{\tt haystack}| \f$
 ///   2. \f$ {\tt index} = -1 \Leftrightarrow \lnot contains\f$
-///   3. \f$ contains \Rightarrow ({\tt index} \le {\tt from\_index} \land
-///          {\tt haystack}[i] = {\tt needle} )\f$
-///   4. \f$ \forall n \in [{\tt index} +1, {\tt from\_index}+1)
+///   3. \f$ contains \Rightarrow
+///          {\tt haystack}[{\tt index}] = {\tt needle} )\f$
+///   4. \f$ \forall n \in [{\tt index} +1,
+///                         min({\tt from\_index}+1, |{\tt haystack}|))
 ///          .\ contains \Rightarrow {\tt haystack}[n] \ne {\tt needle} \f$
-///   5. \f$ \forall m \in [0, {\tt from\_index}+1)
+///   5. \f$ \forall m \in [0,
+///          min({\tt from\_index}+1, |{\tt haystack}|))
 ///          .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}\f$
 /// \param str: an array of characters expression
 /// \param c: a character expression
@@ -314,42 +331,41 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const exprt &from_index)
 {
   const typet &index_type = str.length().type();
-  symbol_exprt index=fresh_exist_index("last_index_of", index_type);
-  symbol_exprt contains=fresh_boolean("contains_in_last_index_of");
+  const symbol_exprt index = fresh_exist_index("last_index_of", index_type);
+  const symbol_exprt contains = fresh_boolean("contains_in_last_index_of");
 
-  exprt index1=from_integer(1, index_type);
-  exprt minus1=from_integer(-1, index_type);
-  exprt from_index_plus_one=plus_exprt_with_overflow_check(from_index, index1);
-  and_exprt a1(
+  const exprt minus1 = from_integer(-1, index_type);
+  const and_exprt a1(
     binary_relation_exprt(index, ID_ge, minus1),
-    binary_relation_exprt(index, ID_lt, from_index_plus_one));
+    binary_relation_exprt(index, ID_le, from_index),
+    binary_relation_exprt(index, ID_lt, str.length()));
   axioms.push_back(a1);
 
-  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
+  const notequal_exprt a2(contains, equal_exprt(index, minus1));
   axioms.push_back(a2);
 
-  implies_exprt a3(
-    contains,
-    and_exprt(
-      binary_relation_exprt(from_index, ID_ge, index),
-      equal_exprt(str[index], c)));
+  const implies_exprt a3(contains, equal_exprt(str[index], c));
   axioms.push_back(a3);
 
-  symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type);
-  string_constraintt a4(
+  const exprt index1 = from_integer(1, index_type);
+  const plus_exprt from_index_plus_one(from_index, index1);
+  const if_exprt end_index(
+    binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
+    from_index_plus_one,
+    str.length());
+
+  const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
+  const string_constraintt a4(
     n,
     plus_exprt(index, index1),
-    from_index_plus_one,
+    end_index,
     contains,
-    not_exprt(equal_exprt(str[n], c)));
+    notequal_exprt(str[n], c));
   axioms.push_back(a4);
 
-  symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type);
-  string_constraintt a5(
-    m,
-    from_index_plus_one,
-    not_exprt(contains),
-    not_exprt(equal_exprt(str[m], c)));
+  const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
+  const string_constraintt a5(
+    m, end_index, not_exprt(contains), notequal_exprt(str[m], c));
   axioms.push_back(a5);
 
   return index;
@@ -384,9 +400,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const typet &char_type = str.content().type().subtype();
   PRECONDITION(f.type() == index_type);
 
-  const exprt from_index =
-    args.size() == 2 ? minus_exprt(str.length(), from_integer(1, index_type))
-                     : args[2];
+  const exprt from_index = args.size() == 2 ? str.length() : args[2];
 
   if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
   {