diff --git a/jbmc/regression/jbmc-strings/StringFormat/Test.class b/jbmc/regression/jbmc-strings/StringFormat/Test.class
index 4620e0f976f..2959bc9fa29 100644
Binary files a/jbmc/regression/jbmc-strings/StringFormat/Test.class and b/jbmc/regression/jbmc-strings/StringFormat/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/StringFormat/Test.java b/jbmc/regression/jbmc-strings/StringFormat/Test.java
index 8dd33a0e98f..98b5d43ac97 100644
--- a/jbmc/regression/jbmc-strings/StringFormat/Test.java
+++ b/jbmc/regression/jbmc-strings/StringFormat/Test.java
@@ -49,4 +49,14 @@ public static String string3(String s, String t) {
     assert(s.length() != 1 || u.charAt(0) == u.charAt(u.length() - 1));
     return u;
   }
+
+  public static String float1(float f) {
+    String u = String.format("Pi is %.2f.", 3.14);
+    // We are not checking the exactness of the string produced, just that
+    // the solver will not crash.
+    assert(u.length() > 0);
+    assert(u.charAt(0) == 'P');
+    return u;
+  }
+
 }
diff --git a/jbmc/regression/jbmc-strings/StringFormat/test-float1.desc b/jbmc/regression/jbmc-strings/StringFormat/test-float1.desc
new file mode 100644
index 00000000000..0975e43d6a6
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringFormat/test-float1.desc
@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.float1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+
diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp
index a8c67b4858b..a6a48a8c34f 100644
--- a/src/solvers/strings/string_constraint_generator_format.cpp
+++ b/src/solvers/strings/string_constraint_generator_format.cpp
@@ -198,7 +198,7 @@ static format_specifiert format_specifier_of_match(std::smatch &m)
   int index = m[1].str().empty() ? -1 : std::stoi(m[1].str());
   std::string flag = m[2].str();
   int width = m[3].str().empty() ? -1 : std::stoi(m[3].str());
-  int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str());
+  int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str().substr(1));
   std::string tT = m[5].str();
 
   bool dt = !tT.empty();