From 441c53b1a68cc16a345eb0dc8d9956c1301ed509 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 3 May 2021 19:07:52 -0700 Subject: FP: Move removal of generic to_fp operations to rewriter. (#6480) --- test/regress/regress0/fp/issue3582.smt2 | 1 + test/regress/regress0/fp/issue5511.smt2 | 1 + test/regress/regress0/fp/issue5734.smt2 | 7 +++++++ test/regress/regress0/fp/issue6164.smt2 | 1 + 4 files changed, 10 insertions(+) create mode 100644 test/regress/regress0/fp/issue5734.smt2 (limited to 'test/regress/regress0/fp') 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) -- cgit v1.2.3