Actively split for upwards closusure intersection. Minor clean up, add regressions.

4 files changed, 33 insertions, 2 deletions

diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index 7c9dca8dd..bb9c49298 100644
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -101,7 +101,8 @@ TESTS =	\
   rel_transpose_0.cvc \
   set-strat.cvc \
   rel_tc_8.cvc \
-  atom_univ2.cvc
+  atom_univ2.cvc \
+  rels-sharing-simp.cvc
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc b/test/regress/regress0/rels/rels-sharing-simp.cvc
new file mode 100644
index 000000000..26bc94a43
--- /dev/null
+++ b/test/regress/regress0/rels/rels-sharing-simp.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+z : SET OF IntPair;
+x : INT;
+y : INT;
+
+ASSERT (1,x) IS_IN w;
+ASSERT (y,2) IS_IN z;
+
+ASSERT NOT (1, 2) IS_IN ( w JOIN z );
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 4c65f3a6a..c2e3546d9 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -78,7 +78,8 @@ TESTS =	\
 	univset-simp.smt2 \
 	complement.cvc \
 	complement2.cvc \
-    complement3.cvc
+  complement3.cvc \
+  sharing-simp.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2
new file mode 100644
index 000000000..761428fde
--- /dev/null
+++ b/test/regress/regress0/sets/sharing-simp.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun C () (Set Int))
+(declare-fun D () (Set Int))
+
+(assert (member x A))
+(assert (member y B))
+(assert (or (= C (intersection A B)) (= D (intersection A B))))
+
+
+(check-sat)