diff --git a/jbmc/regression/jbmc/double1/double1.class b/jbmc/regression/jbmc/double1/double1.class
index e96fdb5e513..7d62e4f55b9 100644
Binary files a/jbmc/regression/jbmc/double1/double1.class and b/jbmc/regression/jbmc/double1/double1.class differ
diff --git a/jbmc/regression/jbmc/double1/double1.java b/jbmc/regression/jbmc/double1/double1.java
index f71435b7641..23d93024d5e 100644
--- a/jbmc/regression/jbmc/double1/double1.java
+++ b/jbmc/regression/jbmc/double1/double1.java
@@ -19,5 +19,13 @@ public static void main(String[] args)
     d=java.lang.Double.NEGATIVE_INFINITY;
     d=java.lang.Double.NaN;
   }
+
+  public static String testLimit(double inputValue) {
+    if(0x1p-1022 == inputValue){
+      assert(false);
+      return "reach";
+    }
+    return "default";
+  }
 }
 
diff --git a/jbmc/regression/jbmc/double1/test-limit.desc b/jbmc/regression/jbmc/double1/test-limit.desc
new file mode 100644
index 00000000000..cd8817af619
--- /dev/null
+++ b/jbmc/regression/jbmc/double1/test-limit.desc
@@ -0,0 +1,11 @@
+CORE
+double1.class
+ --function double1.testLimit --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+INPUT arg0d: 0x1(\.0*)?p-1022 /\* 2.22507e-308
+--
+^warning: ignoring
+--
+Test double value are printed with sufficient precision
diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h
index a602b612a44..42339ff8782 100644
--- a/jbmc/src/java_bytecode/expr2java.h
+++ b/jbmc/src/java_bytecode/expr2java.h
@@ -79,8 +79,6 @@ std::string floating_point_to_java_string(float_type value)
     return raw_decimal;
   }();
   const bool is_lossless = [&] {
-    if(value == std::numeric_limits<float_type>::min())
-      return true;
     try
     {
       return std::stod(decimal) == value;