diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-05-17 21:36:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-05-17 21:36:37 -0500 |
| commit | 28c52d96da9107199d0fd57ab9c3098089e99fd1 (patch) | |
| tree | 7fa9490f567b7196b1551721311525c55abb6694 /test/regress/regress0 | |
| parent | 0baa03948e9ed558dd1884acba5f7c9b5e151071 (diff) | |
| parent | 521701398b15bd41a1cb8a9b530fc4af4892c7af (diff) | |
Merge branch 'master' into optimizeRunscriptSLIAoptimizeRunscriptSLIA
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/fp/down-cast-RNA.smt2 | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2 new file mode 100644 index 000000000..d14c63be5 --- /dev/null +++ b/test/regress/regress0/fp/down-cast-RNA.smt2 @@ -0,0 +1,24 @@ +; REQUIRES: symfpu +; COMMAND-LINE: --fp-exp +; EXPECT: unsat + +(set-logic QF_FP) +(set-info :source |Written by Andres Noetzli for issue #2183|) +(set-info :smt-lib-version 2.5) +(set-info :category crafted) +(set-info :status unsat) + +(declare-fun r () (_ FloatingPoint 5 9)) +(declare-fun rr () (_ FloatingPoint 5 9) ((_ to_fp 5 9) RNA (fp #b1 #b00000 #b1111111110))) + +; Let's work out this one out manually +; #b1111111110 is an significand of +; 11111111110, rounding positions (g for guard, s for sticky) +; 123456789gs +; so g = 1, s = 0 which is the tie break case +; RNA says tie break goes away from zero, so this is a round up +; incrementing the significand carries up so the true result should be +; (fp #b1 #b00001 #x00000000) + +(assert (= (fp #b1 #b00000 #xff) rr)) +(check-sat) |