diff --git a/frontends/benchmarks/verification/valid/FPFledging.scala b/frontends/benchmarks/verification/valid/FPFledging.scala
new file mode 100644
index 0000000000..ac1ca88181
--- /dev/null
+++ b/frontends/benchmarks/verification/valid/FPFledging.scala
@@ -0,0 +1,21 @@
+import stainless.math._
+
+object FPFledging {
+  def test1(x: Double): Unit = {
+    assert(Double.longBitsToDouble(Double.doubleToRawLongBits(x)) == x)
+  }
+
+  def test2(x: Long): Unit = {
+    Double.longBitsToDoublePost(x)
+    assert(Double.doubleToRawLongBits(Double.longBitsToDouble(x)) == x)
+  }
+
+  def test3(x: Float): Unit = {
+    assert(Float.intBitsToFloat(Float.floatToRawIntBits(x)) == x)
+  }
+
+  def test4(x: Int): Unit = {
+    Float.intBitsToFloatPost(x)
+    assert(Float.floatToRawIntBits(Float.intBitsToFloat(x)) == x)
+  }
+}
\ No newline at end of file
diff --git a/frontends/library/stainless/math/Double.scala b/frontends/library/stainless/math/Double.scala
new file mode 100644
index 0000000000..bc25fe540f
--- /dev/null
+++ b/frontends/library/stainless/math/Double.scala
@@ -0,0 +1,26 @@
+package stainless
+package math
+
+import lang.StaticChecks._
+import annotation._
+
+@library
+case class Double(@extern @pure private val value: scala.Double) extends AnyVal
+
+@library
+object Double {
+  @extern @pure
+  def longBitsToDouble(l: Long): Double = {
+    Double(java.lang.Double.longBitsToDouble(l))
+  }
+
+  @extern @pure
+  def longBitsToDoublePost(l: Long): Unit = {
+    ()
+  } ensuring (_ => doubleToRawLongBits(longBitsToDouble(l)) == l)
+
+  @extern @pure
+  def doubleToRawLongBits(d: Double): Long = {
+    java.lang.Double.doubleToRawLongBits(d.value)
+  } ensuring (res => longBitsToDouble(res) == d)
+}
\ No newline at end of file
diff --git a/frontends/library/stainless/math/Float.scala b/frontends/library/stainless/math/Float.scala
new file mode 100644
index 0000000000..9d18b9a36e
--- /dev/null
+++ b/frontends/library/stainless/math/Float.scala
@@ -0,0 +1,26 @@
+package stainless
+package math
+
+import lang.StaticChecks._
+import annotation._
+
+@library
+case class Float(@extern @pure private val value: scala.Float) extends AnyVal
+
+@library
+object Float {
+  @extern @pure
+  def intBitsToFloat(i: Int): Float = {
+    Float(java.lang.Float.intBitsToFloat(i))
+  }
+
+  @extern @pure
+  def intBitsToFloatPost(i: Int): Unit = {
+    ()
+  } ensuring (_ => floatToRawIntBits(intBitsToFloat(i)) == i)
+
+  @extern @pure
+  def floatToRawIntBits(d: Float): Int = {
+    java.lang.Float.floatToRawIntBits(d.value)
+  } ensuring (res => intBitsToFloat(res) == d)
+}
\ No newline at end of file
diff --git a/libfiles.txt b/libfiles.txt
index 0ef19b063a..7039c5172a 100644
--- a/libfiles.txt
+++ b/libfiles.txt
@@ -20,6 +20,8 @@ stainless/covcollection/Option.scala
 stainless/equations/package.scala
 stainless/math/BitVectors.scala
 stainless/math/Nat.scala
+stainless/math/Float.scala
+stainless/math/Double.scala
 stainless/math/package.scala
 stainless/io/FileOutputStream.scala
 stainless/io/StdOut.scala