FP: Move removal of generic to_fp operations to rewriter. (#6480)

5 files changed, 11 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 685ac8b4e..3f1ff1307 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -581,6 +581,7 @@ set(regress_0_tests
   regress0/fp/issue3619.smt2
   regress0/fp/issue4277-assign-func.smt2
   regress0/fp/issue5511.smt2
+  regress0/fp/issue5734.smt2
   regress0/fp/issue6164.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
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)