diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp
index daa89f21a98..60bc6273dae 100644
--- a/src/java_bytecode/expr2java.cpp
+++ b/src/java_bytecode/expr2java.cpp
@@ -8,12 +8,14 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 
 #include <cassert>
+#include <sstream>
 
 #include <util/namespace.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
 #include <util/arith_tools.h>
+#include <util/ieee_float.h>
 
 #include <ansi-c/c_qualifiers.h>
 #include <ansi-c/c_misc.h>
@@ -235,6 +237,63 @@ std::string expr2javat::convert_constant(
     dest+='L';
     return dest;
   }
+  else if((src.type()==java_float_type()) ||
+          (src.type()==java_double_type()))
+  {
+    ieee_floatt ieee_repr(to_constant_expr(src));
+    std::string result;
+
+    bool float_flag=(src.type()==java_float_type());
+    if(ieee_repr.is_zero())
+    {
+      result+='0';
+      format_spect fs;
+      if(fs.precision>0)
+      {
+        result+='.';
+        for(std::size_t i=0; i<fs.precision; i++)
+          result+='0';
+        if(float_flag)
+          result+='f';
+      }
+      return(result);
+    }
+
+    if(ieee_repr.is_NaN())
+    {
+       if(float_flag)
+         return("Float.NaN");
+       else
+         return("Double.NaN");
+    }
+
+    if(ieee_repr.is_infinity())
+    {
+      if(float_flag)
+      {
+        if(ieee_repr.get_sign())
+          return("Float.NEGATIVE_INFINITY");
+        else
+          return("Float.POSITIVE_INFINITY");
+      }
+      else
+      {
+        if(ieee_repr.get_sign())
+          return("Double.NEGATIVE_INFINITY");
+        else
+          return("Double.POSITIVE_INFINITY");
+      }
+    }
+
+    std::stringstream buffer;
+    buffer << std::hexfloat;
+    if(float_flag)
+      buffer << ieee_repr.to_float() << 'f';
+    else
+      buffer << ieee_repr.to_double();
+    return(buffer.str());
+  }
+
 
   return expr2ct::convert_constant(src, precedence);
 }