diff --git a/regression/cbmc/Float-rounding2/main.c b/regression/cbmc/Float-rounding2/main.c
new file mode 100644
index 00000000000..a73715a6c5f
--- /dev/null
+++ b/regression/cbmc/Float-rounding2/main.c
@@ -0,0 +1,27 @@
+#include <assert.h>
+
+int main()
+{
+#if 0
+  // examples of constants that previously exhibited wrong behaviour
+  union U
+  {
+    double d;
+    uint64_t b;
+  };
+  union U u = {
+    .b = 0b0000000000000011111111111111111111111110000001000000000000000000};
+  union U u2 = {
+    .b = 0b0000000000000000000000000000001111111111111111111111111000000000};
+  double d = u.d;
+#else
+  double d;
+#endif
+  float f;
+  if(d > 0.0 && d < 1.0)
+  {
+    f = d;
+    assert(f <= 1.0f);
+  }
+  return 0;
+}
diff --git a/regression/cbmc/Float-rounding2/test.desc b/regression/cbmc/Float-rounding2/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/Float-rounding2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
index 43dee046246..3611abd3632 100644
--- a/src/solvers/floatbv/float_bv.cpp
+++ b/src/solvers/floatbv/float_bv.cpp
@@ -458,7 +458,14 @@ exprt float_bvt::conversion(
     // if the number was denormal and is normal in the new format,
     // normalise it!
     if(dest_spec.e > src_spec.e)
+    {
       normalization_shift(result.fraction, result.exponent);
+      // normalization_shift unconditionally extends the exponent size to avoid
+      // arithmetic overflow, but this cannot have happened here as the exponent
+      // had already been extended to dest_spec's size
+      result.exponent =
+        typecast_exprt(result.exponent, signedbv_typet(dest_spec.e));
+    }
 
     // the flags get copied
     result.sign=unpacked_src.sign;
@@ -954,8 +961,8 @@ void float_bvt::normalization_shift(
 
   std::size_t depth = address_bits(fraction_bits - 1);
 
-  if(exponent_bits<depth)
-    exponent=typecast_exprt(exponent, signedbv_typet(depth));
+  exponent = typecast_exprt(
+    exponent, signedbv_typet(std::max(depth, exponent_bits + 1)));
 
   exprt exponent_delta=from_integer(0, exponent.type());
 
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index cd3a246b031..13706f06bd5 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -195,6 +195,10 @@ bvt float_utilst::conversion(
     if(dest_spec.e > spec.e)
     {
       normalization_shift(result.fraction, result.exponent);
+      // normalization_shift unconditionally extends the exponent size to avoid
+      // arithmetic overflow, but this cannot have happened here as the exponent
+      // had already been extended to dest_spec's size
+      result.exponent.resize(dest_spec.e);
     }
 
     // the flags get copied
@@ -792,8 +796,9 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
   PRECONDITION(!fraction.empty());
   std::size_t depth = address_bits(fraction.size() - 1);
 
-  if(exponent.size()<depth)
-    exponent=bv_utils.sign_extension(exponent, depth);
+  // sign-extend to ensure the arithmetic below cannot result in overflow/underflow
+  exponent =
+    bv_utils.sign_extension(exponent, std::max(depth, exponent.size() + 1));
 
   bvt exponent_delta=bv_utils.zeros(exponent.size());