diff options
| author | Martin <martin.brain@cs.ox.ac.uk> | 2019-05-21 18:49:37 +0100 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-21 10:49:37 -0700 |
| commit | 1c1c178db1755a441792d84465dcb8397f1f2011 (patch) | |
| tree | 3c9f0d90bf2aabb0bab790767ad5de5170e985e2 /test/regress/regress0 | |
| parent | 16ade2e20b6fd2afc49b8ea70d128ae665dff409 (diff) | |
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.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/fp/rti_3_5_bug.smt2 | 25 | ||||
| -rw-r--r-- | test/regress/regress0/fp/rti_3_5_bug_report.smt2 | 20 |
2 files changed, 45 insertions, 0 deletions
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)
|