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.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c3f2bc866d7cd116a3d42d2ace92e64ea691b174..c920f21a9f4bb94df3d7b2e44c8f68a6c39423df 100644 (file)
--- 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 (file)
index 0000000..d14c63b
--- /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)