1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
new file mode 100644
index 000000000..d01b7468e
--- /dev/null
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet ()
+  (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+(declare-fun x () Int)
+
+(assert (or (not (= S smt_set_emp)) (in x T)))
+
+(assert (= smt_set_emp 
+           (ite (in x T) 
+                (union (union smt_set_emp (setenum x)) S) 
+                S)))
+(check-sat)