1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2
new file mode 100644
index 000000000..13ca789f6
--- /dev/null
+++ b/test/regress/regress1/sets/issue2904.smt2
@@ -0,0 +1,27 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+; conjecture set nonempty(~b & ~c)
+
+(declare-fun n () Int)
+(declare-fun f () Int)
+(declare-fun m () Int)
+
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun UNIVERALSET () (Set Int))
+(assert (subset b UNIVERALSET))
+(assert (subset c UNIVERALSET))
+
+(assert (> n 0))
+(assert (= (card UNIVERALSET) n))
+(assert (= (card b) m))
+(assert (= (card c) (- f m)))
+(assert (>= m 0))
+(assert (>= f m))
+(assert (> n (+ (* 2 f) m)))
+
+
+(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n))
+
+(check-sat)