7 files changed, 53 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5a557a8a3..7e35487af 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -573,10 +573,16 @@ set(regress_0_tests
   regress0/fp/abs-unsound2.smt2
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
+  regress0/fp/from_ubv.smt2
+  regress0/fp/from_sbv.smt2
   regress0/fp/issue-5524.smt2
   regress0/fp/issue3536.smt2
+  regress0/fp/issue3582.smt2
   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
   regress0/fp/wrong-model.smt2
diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2
new file mode 100644
index 000000000..226d6589c
--- /dev/null
+++ b/test/regress/regress0/fp/from_sbv.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fp-exp
+; EXPECT: unsat
+(set-logic QF_BVFP)
+(declare-const x (_ BitVec 1))
+(declare-const rm RoundingMode)
+(assert (or
+  (distinct ((_ to_fp 5 11) rm #b1) (fp #b1 #b01111 #b0000000000))
+  (distinct ((_ to_fp 5 11) rm #b0) (_ +zero 5 11))
+  (ite
+     (= x #b1)
+     (= ((_ to_fp 5 11) rm x) ((_ to_fp_unsigned 5 11) rm x))
+     (distinct ((_ to_fp 5 11) rm x) ((_ to_fp_unsigned 5 11) rm x))
+  )
+  ))
+(check-sat)
diff --git a/test/regress/regress0/fp/from_ubv.smt2 b/test/regress/regress0/fp/from_ubv.smt2
new file mode 100644
index 000000000..6939e478a
--- /dev/null
+++ b/test/regress/regress0/fp/from_ubv.smt2
@@ -0,0 +1,5 @@
+; EXPECT: unsat
+(set-logic QF_FP)
+(declare-const r RoundingMode)
+(assert (distinct ((_ to_fp_unsigned 8 24) r (_ bv0 1)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))
+(check-sat)
diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2
new file mode 100644
index 000000000..2de76b680
--- /dev/null
+++ b/test/regress/regress0/fp/issue3582.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+(set-logic QF_FP)
+(declare-fun bv () (_ BitVec 1))
+(define-fun x () (_ FloatingPoint 11 53) ((_ to_fp_unsigned 11 53) RNE bv))
+(assert (fp.isNaN x))
+(check-sat)
diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2
new file mode 100644
index 000000000..d4393486c
--- /dev/null
+++ b/test/regress/regress0/fp/issue5511.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: symfpu
+; EXPECT: sat
+(set-logic QF_FP)
+(declare-fun a () (_ FloatingPoint 53 11))
+(assert (= a (_ +oo 53 11)))
+(check-sat)
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
new file mode 100644
index 000000000..056a98afc
--- /dev/null
+++ b/test/regress/regress0/fp/issue6164.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: symfpu
+; EXPECT: sat
+; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110)))
+(set-logic ALL)
+(set-option :produce-models true)
+(check-sat)
+(get-value (((_ to_fp 5 11) RNA 0.1)))