diff --git a/regression/cbmc/Float-to-int1/main.c b/regression/cbmc/Float-to-int1/main.c
new file mode 100644
index 00000000000..a5400c4057f
--- /dev/null
+++ b/regression/cbmc/Float-to-int1/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+double nondet_double();
+
+int main(void)
+{
+  double d = nondet_double();
+
+  __CPROVER_assume(d < 0x1.0p+63 && d > 0x1.0p+53);
+
+  long long int i = d;
+  double d1 = i;
+
+  assert(d1 != 0x0);
+
+  return 0;
+}
+
diff --git a/regression/cbmc/Float-to-int1/test.desc b/regression/cbmc/Float-to-int1/test.desc
new file mode 100644
index 00000000000..b7d95a28215
--- /dev/null
+++ b/regression/cbmc/Float-to-int1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Float-to-int2/main.c b/regression/cbmc/Float-to-int2/main.c
new file mode 100644
index 00000000000..cd2e7a7a92b
--- /dev/null
+++ b/regression/cbmc/Float-to-int2/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int nondet_int();
+double nondet_double();
+
+int main(void)
+{
+  int i = nondet_int();
+  double di = (double)i;
+  int j = (int)di;
+
+  assert(i == j);
+
+  return 0;
+}
+
diff --git a/regression/cbmc/Float-to-int2/test.desc b/regression/cbmc/Float-to-int2/test.desc
new file mode 100644
index 00000000000..b7d95a28215
--- /dev/null
+++ b/regression/cbmc/Float-to-int2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Float-to-int3/main.c b/regression/cbmc/Float-to-int3/main.c
new file mode 100644
index 00000000000..0dce5d0ddbf
--- /dev/null
+++ b/regression/cbmc/Float-to-int3/main.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdint.h>
+
+int64_t nondet_int64_t();
+double nondet_double();
+
+int main(void)
+{
+  int64_t i = nondet_int64_t();
+
+  __CPROVER_assume((i & (int64_t)0x7FF) == (int64_t)0);
+  
+  double di = (double)i;
+  int64_t j = (int64_t)di;
+
+  assert(i == j);
+
+  return 0;
+}
+
diff --git a/regression/cbmc/Float-to-int3/test.desc b/regression/cbmc/Float-to-int3/test.desc
new file mode 100644
index 00000000000..b7d95a28215
--- /dev/null
+++ b/regression/cbmc/Float-to-int3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index e71777fdf75..1b3bbf81f1d 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -159,10 +159,21 @@ bvt float_utilst::to_integer(
   // The following is the usual case in ANSI-C, and we optimize for that.
   if(rounding_mode_bits.round_to_zero.is_true())
   {
+    bvt fraction=unpacked.fraction;
+
+    if(dest_width>fraction.size())
+    {
+      bvt lsb_extension=bv_utils.build_constant(0U, dest_width-fraction.size());
+      fraction.insert(fraction.begin(),
+                      lsb_extension.begin(),
+                      lsb_extension.end());
+    }
+
     // if the exponent is positive, shift right
-    bvt offset=bv_utils.build_constant(spec.f, unpacked.exponent.size());
+    bvt offset=bv_utils.build_constant(fraction.size()-1,
+                                       unpacked.exponent.size());
     bvt distance=bv_utils.sub(offset, unpacked.exponent);
-    bvt shift_result=bv_utils.shift(unpacked.fraction, bv_utilst::LRIGHT, distance);
+    bvt shift_result=bv_utils.shift(fraction, bv_utilst::LRIGHT, distance);
 
     // if the exponent is negative, we have zero anyways
     bvt result=shift_result;
@@ -176,11 +187,6 @@ bvt float_utilst::to_integer(
     {
       result.resize(dest_width);
     }
-    else if(result.size()<dest_width)
-    {
-      // zero extend
-      result=bv_utils.zero_extension(result, dest_width);
-    }
 
     assert(result.size()==dest_width);