diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-03 19:07:52 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-04 02:07:52 +0000 |
commit | 441c53b1a68cc16a345eb0dc8d9956c1301ed509 (patch) | |
tree | 81bd2ad3b42a61ed106c695a71c073e17af8da8e /test/regress/regress0/fp | |
parent | ebcddc25124fe3f92df314c13b3d690b46dbd1e8 (diff) |
FP: Move removal of generic to_fp operations to rewriter. (#6480)
Diffstat (limited to 'test/regress/regress0/fp')
-rw-r--r-- | test/regress/regress0/fp/issue3582.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue5511.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue5734.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue6164.smt2 | 1 |
4 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2 index c06cdb110..2de76b680 100644 --- a/test/regress/regress0/fp/issue3582.smt2 +++ b/test/regress/regress0/fp/issue3582.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-fun bv () (_ BitVec 1)) diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2 index 911db54ee..d4393486c 100644 --- a/test/regress/regress0/fp/issue5511.smt2 +++ b/test/regress/regress0/fp/issue5511.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () (_ FloatingPoint 53 11)) diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2 new file mode 100644 index 000000000..2ad9ac921 --- /dev/null +++ b/test/regress/regress0/fp/issue5734.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: symfpu +; EXPECT: sat +(set-logic QF_FP) +(declare-fun a () RoundingMode) +(declare-fun b () (_ FloatingPoint 8 24)) +(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0)) b)))) +(check-sat) diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2 index 3ec9f1594..056a98afc 100644 --- a/test/regress/regress0/fp/issue6164.smt2 +++ b/test/regress/regress0/fp/issue6164.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; EXPECT: sat ; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110))) (set-logic ALL) |