From: Martin <martin.brain@cs.ox.ac.uk>
Date: Fri, 17 May 2019 23:10:19 +0000 (+0100)
Subject: Add the problematic input from issue 2183 as a regression test (#3008)
X-Git-Tag: cvc5-1.0.0~4145
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c38c59cb40df00e29cbd9d30495833f88c6d4fb;p=cvc5.git

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 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)