From 5c38c59cb40df00e29cbd9d30495833f88c6d4fb Mon Sep 17 00:00:00 2001 From: Martin Date: Sat, 18 May 2019 00:10:19 +0100 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/down-cast-RNA.smt2 | 24 +++++++++++++++++++++ 2 files changed, 25 insertions(+) create mode 100644 test/regress/regress0/fp/down-cast-RNA.smt2 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) -- 2.30.2