1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2
new file mode 100644
index 000000000..56f7e8c5e
--- /dev/null
+++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun a () (Set Real))
+
+(declare-fun x () Real)
+
+(assert (= (as univset (Set Real)) (as univset (Set Int))))
+
+(assert (member x a))
+
+(assert (and (<= 5.5 x) (< x 5.8)))
+
+(check-sat)