diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index cdb413e351e..3cda7db79d0 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -709,9 +709,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      ieee_floatt f(to_floatbv_type(expr.type()));
-      f.from_integer(1);
-      result=f.pack();
+      result = ieee_floatt::one(to_floatbv_type(expr.type())).pack();
     }
     else
       result=1;
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 3be48023153..84d25cc8883 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -204,10 +204,8 @@ bool boolbvt::type_conversion(
         // bool to float
 
         // build a one
-        ieee_floatt f(to_floatbv_type(dest_type));
-        f.from_integer(1);
-
-        dest = convert_bv(f.to_expr());
+        auto one = ieee_floatt::one(to_floatbv_type(dest_type));
+        dest = convert_bv(one.to_expr());
 
         INVARIANT(
           src_width == 1, "bitvector of type boolean shall have width one");
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 3662b8f5e1e..dba907efd9d 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -3064,32 +3064,13 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
 
     if(src_type.id()==ID_bool)
     {
-      constant_exprt val(irep_idt(), dest_type);
-
-      ieee_floatt a(dest_floatbv_type);
-
-      mp_integer significand;
-      mp_integer exponent;
-
       out << "(ite ";
       convert_expr(src);
-      out << " ";
-
-      significand = 1;
-      exponent = 0;
-      a.build(significand, exponent);
-      val.set_value(integer2bvrep(a.pack(), a.spec.width()));
-
-      convert_constant(val);
-      out << " ";
-
-      significand = 0;
-      exponent = 0;
-      a.build(significand, exponent);
-      val.set_value(integer2bvrep(a.pack(), a.spec.width()));
-
-      convert_constant(val);
-      out << ")";
+      out << ' ';
+      convert_constant(ieee_floatt::one(dest_floatbv_type).to_expr());
+      out << ' ';
+      convert_constant(ieee_floatt::zero(dest_floatbv_type).to_expr());
+      out << ')';
     }
     else if(src_type.id()==ID_c_bool)
     {
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 52a507ff958..050e51d03f9 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -470,6 +470,19 @@ void ieee_floatt::extract_base10(
   }
 }
 
+ieee_floatt ieee_floatt::one(const ieee_float_spect &spec)
+{
+  ieee_floatt result{spec};
+  result.exponent = 0;
+  result.fraction = power(2, result.spec.f);
+  return result;
+}
+
+ieee_floatt ieee_floatt::one(const floatbv_typet &type)
+{
+  return one(ieee_float_spect{type});
+}
+
 void ieee_floatt::build(
   const mp_integer &_fraction,
   const mp_integer &_exponent)
diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h
index daf6559fd11..8f1696291b9 100644
--- a/src/util/ieee_float.h
+++ b/src/util/ieee_float.h
@@ -220,6 +220,16 @@ class ieee_floatt
     return result;
   }
 
+  static ieee_floatt zero(const ieee_float_spect &spec)
+  {
+    ieee_floatt result(spec);
+    result.make_zero();
+    return result;
+  }
+
+  static ieee_floatt one(const floatbv_typet &);
+  static ieee_floatt one(const ieee_float_spect &);
+
   void make_NaN();
   void make_plus_infinity();
   void make_minus_infinity();
diff --git a/unit/Makefile b/unit/Makefile
index 087cd3cf460..c665d5b824b 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -150,6 +150,7 @@ SRC += analyses/ai/ai.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \
        util/help_formatter.cpp \
+       util/ieee_float.cpp \
        util/interval/add.cpp \
        util/interval/bitwise.cpp \
        util/interval/comparisons.cpp \
diff --git a/unit/util/ieee_float.cpp b/unit/util/ieee_float.cpp
new file mode 100644
index 00000000000..2776772d1c8
--- /dev/null
+++ b/unit/util/ieee_float.cpp
@@ -0,0 +1,9 @@
+#include <util/ieee_float.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Make an IEEE 754 one", "[core][util][ieee_float]")
+{
+  auto spec = ieee_float_spect::single_precision();
+  REQUIRE(ieee_floatt::one(spec) == 1);
+}