From 02bf2530b5eff6eec23bc0a2b5499998e65771f7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 5 Apr 2018 19:55:41 +0100
Subject: [PATCH] Bugfix for fp.to_sbv. Thanks to Florian Schanda for reporting
 this bug.

---
 src/ast/fpa/fpa2bv_converter.cpp | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 2b09dfe8c..9d8576203 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3241,24 +3241,29 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     dbg_decouple("fpa2bv_to_bv_inc", inc);
     dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
 
-    expr_ref ul(m), ovfl(m), in_range(m);
+    expr_ref incd(m), pr_is_zero(m), ovfl(m);
+    incd = m.mk_eq(rounding_decision, bv1);
+    pr_is_zero = m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz + 3));
+    ovfl = m.mk_and(incd, pr_is_zero);
+
+    expr_ref ul(m), in_range(m);
     if (!is_signed) {
-        expr_ref incd(m), pr_is_zero(m);
-        incd = m.mk_eq(rounding_decision, bv1);
-        pr_is_zero = m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz + 3));
         ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
-        in_range = m.mk_and(m.mk_not(x_is_neg),
-                            m.mk_not(m.mk_and(incd, pr_is_zero)),
+        in_range = m.mk_and(m.mk_not(x_is_neg), m.mk_not(ovfl),
                             m_bv_util.mk_ule(pre_rounded, ul));
     }
     else {
         expr_ref ll(m);
         ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
         ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1));
-        pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
-        in_range = m.mk_and(m.mk_not(ovfl), m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
+        ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_numeral(-1, bv_sz + 3)));
+        in_range = m.mk_and(m.mk_not(ovfl),
+                            m_bv_util.mk_sle(ll, pre_rounded),
+                            m_bv_util.mk_sle(pre_rounded, ul));
         dbg_decouple("fpa2bv_to_bv_in_range_ll", ll);
+        pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
     }
+    dbg_decouple("fpa2bv_to_bv_in_range_ovfl", ovfl);
     dbg_decouple("fpa2bv_to_bv_in_range_ul", ul);
     dbg_decouple("fpa2bv_to_bv_in_range", in_range);