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.

diff --git a/contrib/get-symfpu b/contrib/get-symfpu
index 705e9d873f923190ba53e848c0e02516d8323325..a31d27e06258a54ef021ccd8187fe112511eabcf 100755 (executable)
--- 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 c920f21a9f4bb94df3d7b2e44c8f68a6c39423df..565c45eb78a00bd0dff427910feaa024dc622cd1 100644 (file)
--- 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 (file)
index 0000000..56c11bb
--- /dev/null
+++ b/test/regress/regress0/fp/rti_3_5_bug.smt2
@@ -0,0 +1,25 @@
+; REQUIRES: symfpu\r
+; COMMAND-LINE: --fp-exp\r
+; EXPECT: unsat\r
+\r
+(set-logic QF_FP)\r
+(set-info :source |Written by Martin for issue #2932|)\r
+(set-info :smt-lib-version 2.5)\r
+(set-info :category crafted)\r
+(set-info :status unsat)\r
+\r
+(declare-fun x () (_ FloatingPoint 3 5))\r
+(assert (fp.isPositive x))\r
+\r
+(declare-fun xx () (_ FloatingPoint 3 5))\r
+(assert (= xx (fp.roundToIntegral RNE x)))\r
+\r
+(assert (not (= x xx)))\r
+\r
+(declare-fun xxx () (_ FloatingPoint 3 5))\r
+(assert (= xxx (fp.roundToIntegral RNE xx)))\r
+\r
+(assert (not (= xx xxx)))\r
+\r
+(check-sat)\r
+(exit)\r

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 (file)
index 0000000..5a52ffc
--- /dev/null
+++ b/test/regress/regress0/fp/rti_3_5_bug_report.smt2
@@ -0,0 +1,20 @@
+; REQUIRES: symfpu\r
+; COMMAND-LINE: --fp-exp\r
+; EXPECT: unsat\r
+\r
+(set-logic FP)\r
+(set-info :source |Written by Mathias Preiner for issue #2932|)\r
+(set-info :smt-lib-version 2.5)\r
+(set-info :category crafted)\r
+(set-info :status unsat)\r
+\r
+(define-sort FP () (_ FloatingPoint 3 5))\r
+(declare-const t FP)\r
+(assert\r
+  (distinct\r
+    (= t (fp.roundToIntegral RNA t))  \r
+    (exists ((x FP)) (= (fp.roundToIntegral RNA x) t)) \r
+ )\r
+)\r
+(check-sat)\r
+(exit)\r