From 1c1c178db1755a441792d84465dcb8397f1f2011 Mon Sep 17 00:00:00 2001
From: Martin <martin.brain@cs.ox.ac.uk>
Date: Tue, 21 May 2019 18:49:37 +0100
Subject: [PATCH] Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)

Fixes #2932. fp.roundToIntegral was rounding some very small subnormals up to
between 1 and 2, which is A. wrong and B. not idempotent.  The
corresponding symfpu update fixes this as it was an overflow caused
by the unpacked significand not being able to represent an extra
significand bits.
---
 contrib/get-symfpu                            |  2 +-
 test/regress/CMakeLists.txt                   |  2 ++
 test/regress/regress0/fp/rti_3_5_bug.smt2     | 25 +++++++++++++++++++
 .../regress0/fp/rti_3_5_bug_report.smt2       | 20 +++++++++++++++
 4 files changed, 48 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/fp/rti_3_5_bug.smt2
 create mode 100644 test/regress/regress0/fp/rti_3_5_bug_report.smt2

diff --git a/contrib/get-symfpu b/contrib/get-symfpu
index 705e9d873..a31d27e06 100755
--- a/contrib/get-symfpu
+++ b/contrib/get-symfpu
@@ -9,7 +9,7 @@ if [ -e $wdir ]; then
   exit 1
 fi
 
-commit="1273dc9379b36af1461fe04aa453db82408006cf"
+commit="8fbe139bf0071cbe0758d2f6690a546c69ff0053"
 
 mkdir $wdir
 cd $wdir
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c920f21a9..565c45eb7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -453,6 +453,8 @@ set(regress_0_tests
   regress0/fp/abs-unsound2.smt2
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
+  regress0/fp/rti_3_5_bug.smt2
+  regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/simple.smt2
   regress0/fp/wrong-model.smt2
   regress0/fuzz_1.smt
diff --git a/test/regress/regress0/fp/rti_3_5_bug.smt2 b/test/regress/regress0/fp/rti_3_5_bug.smt2
new file mode 100644
index 000000000..56c11bbf5
--- /dev/null
+++ b/test/regress/regress0/fp/rti_3_5_bug.smt2
@@ -0,0 +1,25 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
+; EXPECT: unsat
+
+(set-logic QF_FP)
+(set-info :source |Written by Martin for issue #2932|)
+(set-info :smt-lib-version 2.5)
+(set-info :category crafted)
+(set-info :status unsat)
+
+(declare-fun x () (_ FloatingPoint 3 5))
+(assert (fp.isPositive x))
+
+(declare-fun xx () (_ FloatingPoint 3 5))
+(assert (= xx (fp.roundToIntegral RNE x)))
+
+(assert (not (= x xx)))
+
+(declare-fun xxx () (_ FloatingPoint 3 5))
+(assert (= xxx (fp.roundToIntegral RNE xx)))
+
+(assert (not (= xx xxx)))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/fp/rti_3_5_bug_report.smt2 b/test/regress/regress0/fp/rti_3_5_bug_report.smt2
new file mode 100644
index 000000000..5a52ffcc9
--- /dev/null
+++ b/test/regress/regress0/fp/rti_3_5_bug_report.smt2
@@ -0,0 +1,20 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
+; EXPECT: unsat
+
+(set-logic FP)
+(set-info :source |Written by Mathias Preiner for issue #2932|)
+(set-info :smt-lib-version 2.5)
+(set-info :category crafted)
+(set-info :status unsat)
+
+(define-sort FP () (_ FloatingPoint 3 5))
+(declare-const t FP)
+(assert
+  (distinct
+    (= t (fp.roundToIntegral RNA t))  
+    (exists ((x FP)) (= (fp.roundToIntegral RNA x) t)) 
+ )
+)
+(check-sat)
+(exit)
-- 
2.30.2