From f6690cead6601c20da21bc73e7841b030ecb3808 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 11 Dec 2016 22:47:30 +0000
Subject: [PATCH] Turn off float constant folding in simplifier

Float constant folding is unsound without
considering the rounding mode.
---
 src/util/simplify_expr_int.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 98dab123a3f..5815e105a60 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -402,6 +402,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
 
   if(ns.follow(expr.type()).id()==ID_floatbv)
   {
+#if 0
     // we only merge neighboring constants!
     Forall_expr(it, operands)
     {
@@ -419,6 +420,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
         }
       }
     }
+#endif
   }
   else
   {