From 84a414ccef1abe9c79e16f50bed341e3e68f3f3d Mon Sep 17 00:00:00 2001
From: kroening <kroening@6afb6bc1-c8e4-404c-8f48-9ae832c5b171>
Date: Wed, 12 Feb 2014 18:47:55 +0000
Subject: [PATCH] Bug in the handling of rounding around underflow

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3598 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
---
 regression/cbmc/Float-no-simp7/main.c    | 13 +++++++++++++
 regression/cbmc/Float-no-simp7/test.desc |  8 ++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc/Float-no-simp7/main.c
 create mode 100644 regression/cbmc/Float-no-simp7/test.desc

diff --git a/regression/cbmc/Float-no-simp7/main.c b/regression/cbmc/Float-no-simp7/main.c
new file mode 100644
index 0000000000..c90e60172a
--- /dev/null
+++ b/regression/cbmc/Float-no-simp7/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main (int argc, char **argv) {
+  float f =  0x1.9e0c22p-101f;
+  float g = -0x1.3c9014p-50f;
+  float target = -0x1p-149f;
+
+  float result = f * g;
+
+  assert(result == target);
+
+  return 0;
+}
diff --git a/regression/cbmc/Float-no-simp7/test.desc b/regression/cbmc/Float-no-simp7/test.desc
new file mode 100644
index 0000000000..4d2a93e6e2
--- /dev/null
+++ b/regression/cbmc/Float-no-simp7/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv --no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring