1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/bounded_sets.smt2 b/test/regress/regress0/fmf/bounded_sets.smt2
new file mode 100644
index 000000000..b06c3636f
--- /dev/null
+++ b/test/regress/regress0/fmf/bounded_sets.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun S () (Set Int))
+(declare-fun P (Int) Bool)
+(declare-fun a () Int)
+(assert (member a S))
+(assert (forall ((y Int)) (=> (member y S) (P y))))
+
+
+(declare-fun T () (Set Int))
+(declare-fun b () Int)
+(assert (member b T))
+(assert (forall ((y Int)) (=> (member y T) (not (P y)))))
+
+(check-sat)