diff --git a/regression/jbmc-strings/StringValueOf09/test.desc b/regression/jbmc-strings/StringValueOf09/test.desc
index d3387709636..583f9fde885 100644
--- a/regression/jbmc-strings/StringValueOf09/test.desc
+++ b/regression/jbmc-strings/StringValueOf09/test.desc
@@ -1,4 +1,4 @@
-THOROUGH
+CORE
 StringValueOf09.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 6cee9ea59b8..35ce5c63225 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -971,7 +971,7 @@ codet java_string_library_preprocesst::make_float_to_string_code(
   exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
 
   // Expression representing 0.0
-  ieee_float_spect float_spec=ieee_float_spect::single_precision();
+  ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
   ieee_floatt zero_float(float_spec);
   zero_float.from_float(0.0);
   constant_exprt zero=zero_float.to_expr();