From 5c38c59cb40df00e29cbd9d30495833f88c6d4fb Mon Sep 17 00:00:00 2001 From: Martin Date: Sat, 18 May 2019 00:10:19 +0100 Subject: 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/regress0/fp/down-cast-RNA.smt2 | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test/regress/regress0/fp/down-cast-RNA.smt2 (limited to 'test/regress/regress0/fp/down-cast-RNA.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) -- cgit v1.2.3