3 files changed, 47 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c920f21a9..565c45eb7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -453,6 +453,8 @@ set(regress_0_tests
   regress0/fp/abs-unsound2.smt2
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
+  regress0/fp/rti_3_5_bug.smt2
+  regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/simple.smt2
   regress0/fp/wrong-model.smt2
   regress0/fuzz_1.smt
diff --git a/test/regress/regress0/fp/rti_3_5_bug.smt2 b/test/regress/regress0/fp/rti_3_5_bug.smt2
new file mode 100644
index 000000000..56c11bbf5
--- /dev/null
+++ b/test/regress/regress0/fp/rti_3_5_bug.smt2
@@ -0,0 +1,25 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
+; EXPECT: unsat
+
+(set-logic QF_FP)
+(set-info :source |Written by Martin for issue #2932|)
+(set-info :smt-lib-version 2.5)
+(set-info :category crafted)
+(set-info :status unsat)
+
+(declare-fun x () (_ FloatingPoint 3 5))
+(assert (fp.isPositive x))
+
+(declare-fun xx () (_ FloatingPoint 3 5))
+(assert (= xx (fp.roundToIntegral RNE x)))
+
+(assert (not (= x xx)))
+
+(declare-fun xxx () (_ FloatingPoint 3 5))
+(assert (= xxx (fp.roundToIntegral RNE xx)))
+
+(assert (not (= xx xxx)))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/fp/rti_3_5_bug_report.smt2 b/test/regress/regress0/fp/rti_3_5_bug_report.smt2
new file mode 100644
index 000000000..5a52ffcc9
--- /dev/null
+++ b/test/regress/regress0/fp/rti_3_5_bug_report.smt2
@@ -0,0 +1,20 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
+; EXPECT: unsat
+
+(set-logic FP)
+(set-info :source |Written by Mathias Preiner for issue #2932|)
+(set-info :smt-lib-version 2.5)
+(set-info :category crafted)
+(set-info :status unsat)
+
+(define-sort FP () (_ FloatingPoint 3 5))
+(declare-const t FP)
+(assert
+  (distinct
+    (= t (fp.roundToIntegral RNA t))  
+    (exists ((x FP)) (= (fp.roundToIntegral RNA x) t)) 
+ )
+)
+(check-sat)
+(exit)