diff options
| author | Martin <martin.brain@cs.ox.ac.uk> | 2019-05-18 00:10:19 +0100 |
|---|---|---|
| committer | Andres Noetzli <noetzli@stanford.edu> | 2019-05-17 16:10:19 -0700 |
| commit | 5c38c59cb40df00e29cbd9d30495833f88c6d4fb (patch) | |
| tree | 5602ee8294a1e4df3bffc0452fe648706cd7748e | |
| parent | 62d361071ea54c9b7cba882313ab4dedef6f1286 (diff) | |
Add the problematic input from issue 2183 as a regression test (#3008)
Although CVC4's behaviour is actually correct, this is to make
things a bit clearer and prevent confusion in the future.
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/down-cast-RNA.smt2 | 24 |
2 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c3f2bc866..c920f21a9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -451,6 +451,7 @@ set(regress_0_tests regress0/fmf/tail_rec.smt2 regress0/fp/abs-unsound.smt2 regress0/fp/abs-unsound2.smt2 + regress0/fp/down-cast-RNA.smt2 regress0/fp/ext-rew-test.smt2 regress0/fp/simple.smt2 regress0/fp/wrong-model.smt2 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) |