New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.

85 files changed, 2662 insertions, 1 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 931228f41..a71cbfe60 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -57,6 +57,7 @@ subdirs_to_check = \
 	regress/regress0/fmf \
 	regress/regress0/strings \
 	regress/regress0/sets \
+	regress/regress0/rels \
 	regress/regress0/parser \
 	regress/regress0/sygus \
 	regress/regress0/sep \
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c790165ef..ec09c9a4a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus sep
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep
 DIST_SUBDIRS = $(SUBDIRS)
 
 # don't override a BINARY imported from a personal.mk
diff --git a/test/regress/regress0/rels/Makefile b/test/regress/regress0/rels/Makefile
new file mode 100644
index 000000000..bd7dc8797
--- /dev/null
+++ b/test/regress/regress0/rels/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/rels
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
new file mode 100644
index 000000000..6b8fdfec7
--- /dev/null
+++ b/test/regress/regress0/rels/Makefile.am
@@ -0,0 +1,115 @@
+SUBDIRS = .
+
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+  addr_book_0.cvc \
+  bv2.cvc \
+  oneLoc_no_quant-int_0_1.cvc \
+  rel_complex_5.cvc \
+  rel_join_3_1.cvc \
+  rel_product_0_1.cvc \
+  rel_tc_10_1.cvc \
+  rel_tc_6.cvc \
+  rel_tp_join_2_1.cvc \
+  rel_transpose_1_1.cvc \
+  strat_0_1.cvc \
+  addr_book_1_1.cvc \
+  prod-mod-eq2.cvc \
+  rel_conflict_0.cvc \
+  rel_join_3.cvc \
+  rel_product_0.cvc \
+  rel_tc_11.cvc \
+  rel_tc_7.cvc \
+  rel_tp_join_2.cvc \
+  rel_transpose_1.cvc \
+  strat.cvc \
+  addr_book_1.cvc \
+  join-eq-structure_0_1.cvc \
+  prod-mod-eq.cvc \
+  rel_join_0_1.cvc \
+  rel_join_4.cvc \
+  rel_product_1_1.cvc \
+  rel_tc_2_1.cvc \
+  rel_tp_join_3.cvc \
+  rel_transpose_3.cvc \
+  bv1.cvc \
+  join-eq-structure-and.cvc \
+  rel_1tup_0.cvc \
+  rel_join_0.cvc \
+  rel_join_5.cvc \
+  rel_product_1.cvc \
+  rel_tc_3_1.cvc \
+  rel_tc_9_1.cvc \
+  rel_tp_join_eq_0.cvc \
+  rel_transpose_4.cvc \
+  bv1p.cvc \
+  join-eq-structure.cvc \
+  rel_complex_0.cvc \
+  rel_join_1_1.cvc \
+  rel_join_6.cvc \
+  rel_symbolic_1_1.cvc \
+  rel_tc_3.cvc \
+  rel_tp_2.cvc \
+  rel_tp_join_int_0.cvc \
+  rel_transpose_5.cvc \
+  bv1p-sat.cvc \
+  join-eq-u.cvc \
+  rel_complex_1.cvc \
+  rel_join_1.cvc \
+  rel_join_7.cvc \
+  rel_symbolic_1.cvc \
+  rel_tc_4_1.cvc \
+  rel_tp_3_1.cvc \
+  rel_tp_join_pro_0.cvc \
+  rel_transpose_6.cvc \
+  bv1-unitb.cvc \
+  join-eq-u-sat.cvc \
+  rel_complex_3.cvc \
+  rel_join_2_1.cvc \
+  rel_mix_0_1.cvc \
+  rel_symbolic_2_1.cvc \
+  rel_tc_4.cvc \
+  rel_tp_join_0.cvc \
+  rel_tp_join_var_0.cvc \
+  rel_transpose_7.cvc \
+  bv1-unit.cvc \
+  rel_complex_4.cvc \
+  rel_join_2.cvc \
+  rel_pressure_0.cvc \
+  rel_symbolic_3_1.cvc \
+  rel_tc_5_1.cvc \
+  rel_tp_join_1.cvc \
+  rel_transpose_0.cvc \
+  set-strat.cvc
+
+# unsolved : garbage_collect.cvc
+# dump-unsat-core crash : rel_tc_8.cvc
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/rels/addr_book_0.cvc b/test/regress/regress0/rels/addr_book_0.cvc
new file mode 100644
index 000000000..5b1ecefd8
--- /dev/null
+++ b/test/regress/regress0/rels/addr_book_0.cvc
@@ -0,0 +1,49 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+AtomTup : TYPE = [Atom];
+AtomBinTup : TYPE = [Atom, Atom];
+AtomTerTup : TYPE = [Atom, Atom, Atom];
+Target: SET OF AtomTup;
+
+Name: SET OF AtomTup;
+Addr: SET OF AtomTup;
+Book: SET OF AtomTup;
+names: SET OF AtomBinTup;
+addr: SET OF AtomTerTup;
+
+b1: Atom;
+b1_tup : AtomTup;
+ASSERT b1_tup = TUPLE(b1);
+ASSERT b1_tup IS_IN Book;
+
+b2: Atom;
+b2_tup : AtomTup;
+ASSERT b2_tup = TUPLE(b2);
+ASSERT b2_tup IS_IN Book;
+
+b3: Atom;
+b3_tup : AtomTup;
+ASSERT b3_tup = TUPLE(b3);
+ASSERT b3_tup IS_IN Book;
+
+n: Atom;
+n_tup : AtomTup;
+ASSERT n_tup = TUPLE(n);
+ASSERT n_tup IS_IN Name;
+
+t: Atom;
+t_tup : AtomTup;
+ASSERT t_tup = TUPLE(t);
+ASSERT t_tup IS_IN Target;
+
+ASSERT ((Book JOIN  addr) JOIN Target) <= Name;
+ASSERT (Book JOIN names) <= Name;
+ASSERT (Name & Addr) = {}::SET OF AtomTup;
+
+ASSERT ({n_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
+ASSERT ({n_tup} JOIN ({b2_tup} JOIN addr)) = ({n_tup} JOIN ({b1_tup} JOIN addr)) | {t_tup};
+ASSERT ({n_tup} JOIN ({b3_tup} JOIN addr)) = ({n_tup} JOIN ({b2_tup} JOIN addr)) - {t_tup};
+ASSERT NOT (({n_tup} JOIN ({b1_tup} JOIN addr)) = ({n_tup} JOIN ({b3_tup} JOIN addr)));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/addr_book_1.cvc b/test/regress/regress0/rels/addr_book_1.cvc
new file mode 100644
index 000000000..34176f274
--- /dev/null
+++ b/test/regress/regress0/rels/addr_book_1.cvc
@@ -0,0 +1,45 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+AtomTup : TYPE = [Atom];
+AtomBinTup : TYPE = [Atom, Atom];
+AtomTerTup : TYPE = [Atom, Atom, Atom];
+Target: SET OF AtomTup;
+
+Name: SET OF AtomTup;
+Addr: SET OF AtomTup;
+Book: SET OF AtomTup;
+names: SET OF AtomBinTup;
+addr: SET OF AtomTerTup;
+
+b1: Atom;
+b1_tup : AtomTup;
+ASSERT b1_tup = TUPLE(b1);
+ASSERT b1_tup IS_IN Book;
+
+b2: Atom;
+b2_tup : AtomTup;
+ASSERT b2_tup = TUPLE(b2);
+ASSERT b2_tup IS_IN Book;
+
+b3: Atom;
+b3_tup : AtomTup;
+ASSERT b3_tup = TUPLE(b3);
+ASSERT b3_tup IS_IN Book;
+
+m: Atom;
+m_tup : AtomTup;
+ASSERT m_tup = TUPLE(m);
+ASSERT m_tup IS_IN Name;
+
+t: Atom;
+t_tup : AtomTup;
+ASSERT t_tup = TUPLE(t);
+ASSERT t_tup IS_IN Target;
+
+ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
+ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)};
+ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)};
+ASSERT NOT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/addr_book_1_1.cvc b/test/regress/regress0/rels/addr_book_1_1.cvc
new file mode 100644
index 000000000..3273ade3a
--- /dev/null
+++ b/test/regress/regress0/rels/addr_book_1_1.cvc
@@ -0,0 +1,45 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+AtomTup : TYPE = [Atom];
+AtomBinTup : TYPE = [Atom, Atom];
+AtomTerTup : TYPE = [Atom, Atom, Atom];
+Target: SET OF AtomTup;
+
+Name: SET OF AtomTup;
+Addr: SET OF AtomTup;
+Book: SET OF AtomTup;
+names: SET OF AtomBinTup;
+addr: SET OF AtomTerTup;
+
+b1: Atom;
+b1_tup : AtomTup;
+ASSERT b1_tup = TUPLE(b1);
+ASSERT b1_tup IS_IN Book;
+
+b2: Atom;
+b2_tup : AtomTup;
+ASSERT b2_tup = TUPLE(b2);
+ASSERT b2_tup IS_IN Book;
+
+b3: Atom;
+b3_tup : AtomTup;
+ASSERT b3_tup = TUPLE(b3);
+ASSERT b3_tup IS_IN Book;
+
+m: Atom;
+m_tup : AtomTup;
+ASSERT m_tup = TUPLE(m);
+ASSERT m_tup IS_IN Name;
+
+t: Atom;
+t_tup : AtomTup;
+ASSERT t_tup = TUPLE(t);
+ASSERT t_tup IS_IN Target;
+
+ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
+ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)};
+ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)};
+ASSERT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/bv1-unit.cvc b/test/regress/regress0/rels/bv1-unit.cvc
new file mode 100644
index 000000000..970ebdc8c
--- /dev/null
+++ b/test/regress/regress0/rels/bv1-unit.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+DATATYPE unit = u END;
+BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BITVECTOR(1);
+b : BITVECTOR(1);
+c : BITVECTOR(1);
+d : BITVECTOR(1);
+e : BITVECTOR(1);
+
+ASSERT NOT ( b = c );
+
+ASSERT (a, u, b) IS_IN x;
+ASSERT (a, u, c) IS_IN x;
+ASSERT (d, u, a) IS_IN y;
+ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/bv1-unitb.cvc b/test/regress/regress0/rels/bv1-unitb.cvc
new file mode 100644
index 000000000..50a5bb48a
--- /dev/null
+++ b/test/regress/regress0/rels/bv1-unitb.cvc
@@ -0,0 +1,22 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+DATATYPE unitb = ub(data : BITVECTOR(1)) END;
+BvPair: TYPE = [BITVECTOR(1), unitb, BITVECTOR(1)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BITVECTOR(1);
+b : BITVECTOR(1);
+c : BITVECTOR(1);
+d : BITVECTOR(1);
+e : BITVECTOR(1);
+u : unitb;
+
+ASSERT NOT ( b = c );
+
+ASSERT (a, u, b) IS_IN x;
+ASSERT (a, u, c) IS_IN x;
+ASSERT (d, u, a) IS_IN y;
+ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/bv1.cvc b/test/regress/regress0/rels/bv1.cvc
new file mode 100644
index 000000000..95e7419ba
--- /dev/null
+++ b/test/regress/regress0/rels/bv1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BITVECTOR(1);
+b : BITVECTOR(1);
+c : BITVECTOR(1);
+d : BITVECTOR(1);
+e : BITVECTOR(1);
+
+ASSERT NOT ( b = c );
+
+ASSERT (a, b) IS_IN x;
+ASSERT (a, c) IS_IN x;
+ASSERT (d, a) IS_IN y;
+ASSERT NOT ( ( a, a ) IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/bv1p-sat.cvc b/test/regress/regress0/rels/bv1p-sat.cvc
new file mode 100644
index 000000000..5eceb214c
--- /dev/null
+++ b/test/regress/regress0/rels/bv1p-sat.cvc
@@ -0,0 +1,22 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BvPair;
+b : BvPair;
+c : BvPair;
+d : BvPair;
+
+ASSERT DISTINCT ( a, b );
+ASSERT DISTINCT ( c, d );
+
+ASSERT a IS_IN x;
+ASSERT b IS_IN x;
+ASSERT a IS_IN y;
+ASSERT b IS_IN y;
+ASSERT NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y));
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/bv1p.cvc b/test/regress/regress0/rels/bv1p.cvc
new file mode 100644
index 000000000..130ccae97
--- /dev/null
+++ b/test/regress/regress0/rels/bv1p.cvc
@@ -0,0 +1,22 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BvPair;
+b : BvPair;
+c : BvPair;
+d : BvPair;
+e : BvPair;
+
+ASSERT DISTINCT ( a, b );
+ASSERT DISTINCT ( c, d, e );
+
+ASSERT a IS_IN x;
+ASSERT b IS_IN x;
+ASSERT a IS_IN y;
+ASSERT b IS_IN y;
+ASSERT (NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)) AND NOT ( e IS_IN (x JOIN y)) );
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/bv2.cvc b/test/regress/regress0/rels/bv2.cvc
new file mode 100644
index 000000000..d7162de7c
--- /dev/null
+++ b/test/regress/regress0/rels/bv2.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+BvPair: TYPE = [BITVECTOR(2), BITVECTOR(2)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BITVECTOR(2);
+b : BITVECTOR(2);
+c : BITVECTOR(2);
+d : BITVECTOR(2);
+e : BITVECTOR(2);
+
+ASSERT NOT ( b = c );
+
+ASSERT (a, b) IS_IN x;
+ASSERT (a, c) IS_IN x;
+ASSERT (d, a) IS_IN y;
+ASSERT NOT ( ( a, a ) IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/garbage_collect.cvc b/test/regress/regress0/rels/garbage_collect.cvc
new file mode 100644
index 000000000..1fc1f2fea
--- /dev/null
+++ b/test/regress/regress0/rels/garbage_collect.cvc
@@ -0,0 +1,60 @@
+% EXPECT: unsat
+H_TYPE: TYPE;
+H: TYPE = [H_TYPE];
+Obj: TYPE;
+Obj_Tup: TYPE = [Obj];
+MARK_TYPE: TYPE = [H_TYPE, Obj];
+RELATE: TYPE = [Obj, Obj];
+REF_TYPE: TYPE = [H_TYPE, Obj, Obj];
+
+% Symbols h0 to h3 are constants of type H that represents the system state;
+h0: SET OF H;
+h1: SET OF H;
+h2: SET OF H;
+h3: SET OF H;
+s0: H_TYPE;
+s1: H_TYPE;
+s2: H_TYPE;
+s3: H_TYPE;
+ASSERT h0 = {TUPLE(s0)};
+ASSERT h1 = {TUPLE(s1)};
+ASSERT h2 = {TUPLE(s2)};
+ASSERT h3 = {TUPLE(s3)};
+
+% ref ⊆ H × Obj × Obj represents references between objects in each state;
+ref : SET OF REF_TYPE;
+
+% mark ⊆ H × Obj represents the marked objects in each state
+mark: SET OF MARK_TYPE;
+
+empty_obj_set: SET OF Obj_Tup;
+ASSERT empty_obj_set = {}:: SET OF Obj_Tup;
+
+% root and live are two constants of type Obj that represents objects;
+root: Obj;
+live: Obj;
+
+% The state transition (h0–h1) resets all the marks
+ASSERT (h1 JOIN mark) = empty_obj_set;
+ASSERT (h0 JOIN ref) <= (h1 JOIN ref);
+
+% (h1–h2) marks objects reachable from root
+ASSERT FORALL (n : Obj) : ((root, n) IS_IN TCLOSURE(h1 JOIN ref)) 
+										  => (TUPLE(n) IS_IN (h2 JOIN mark));
+ASSERT (h1 JOIN ref) <= (h2 JOIN ref);
+
+% (h2–h3) sweeps references of non-marked objects										  
+
+ASSERT FORALL (n: Obj) : (NOT (TUPLE(n) IS_IN (h2 JOIN mark))) 
+										  => ({TUPLE(n)} JOIN (h3 JOIN ref)) = empty_obj_set;										  
+
+ASSERT FORALL (n: Obj) : (TUPLE(n) IS_IN (h2 JOIN mark))
+										  => ({TUPLE(n)} JOIN (h3 JOIN ref)) = ({TUPLE(n)} JOIN (h2 JOIN ref));	
+
+%The safety property is negated, thus it checks if
+%in the final state, there is a live object that was originally reachable from root
+%in the beginning state, but some of its references have been swept 										  
+ASSERT (root, live) IS_IN TCLOSURE(h0 JOIN ref);
+ASSERT NOT (({TUPLE(live)} JOIN (h0 JOIN ref)) <= ({TUPLE(live)} JOIN (h3 JOIN ref)));										  
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/join-eq-structure-and.cvc b/test/regress/regress0/rels/join-eq-structure-and.cvc
new file mode 100644
index 000000000..177410b1e
--- /dev/null
+++ b/test/regress/regress0/rels/join-eq-structure-and.cvc
@@ -0,0 +1,26 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+DATATYPE unit = u END;
+IntUPair: TYPE = [INT, unit];
+UIntPair: TYPE = [unit, INT];
+w : SET OF IntUPair;
+z : SET OF UIntPair;
+
+ASSERT  (x JOIN y) = (w JOIN z) AND (x JOIN y ) = TRANSPOSE(w JOIN z);
+
+ASSERT (0,1) IS_IN (x JOIN y);
+
+t : INT;
+ASSERT t >= 0 AND t <=1;
+s : INT;
+ASSERT s >= 0 AND s <=1;
+
+ASSERT s+t = 1;
+
+ASSERT ( s ,u ) IS_IN w;
+ASSERT NOT ( u, t ) IS_IN z;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/join-eq-structure.cvc b/test/regress/regress0/rels/join-eq-structure.cvc
new file mode 100644
index 000000000..e27d3811c
--- /dev/null
+++ b/test/regress/regress0/rels/join-eq-structure.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+DATATYPE unit = u END;
+IntUPair: TYPE = [INT, unit];
+UIntPair: TYPE = [unit, INT];
+w : SET OF IntUPair;
+z : SET OF UIntPair;
+
+ASSERT  (x JOIN y) = (w JOIN z) OR (x JOIN y ) = TRANSPOSE(w JOIN z);
+
+ASSERT (0,1) IS_IN (x JOIN y);
+
+t : INT;
+ASSERT t >= 0 AND t <=1;
+s : INT;
+ASSERT s >= 0 AND s <=1;
+
+ASSERT s+t = 1;
+
+ASSERT ( s ,u ) IS_IN w;
+ASSERT NOT ( u, t ) IS_IN z;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/join-eq-structure_0_1.cvc b/test/regress/regress0/rels/join-eq-structure_0_1.cvc
new file mode 100644
index 000000000..e27d3811c
--- /dev/null
+++ b/test/regress/regress0/rels/join-eq-structure_0_1.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+DATATYPE unit = u END;
+IntUPair: TYPE = [INT, unit];
+UIntPair: TYPE = [unit, INT];
+w : SET OF IntUPair;
+z : SET OF UIntPair;
+
+ASSERT  (x JOIN y) = (w JOIN z) OR (x JOIN y ) = TRANSPOSE(w JOIN z);
+
+ASSERT (0,1) IS_IN (x JOIN y);
+
+t : INT;
+ASSERT t >= 0 AND t <=1;
+s : INT;
+ASSERT s >= 0 AND s <=1;
+
+ASSERT s+t = 1;
+
+ASSERT ( s ,u ) IS_IN w;
+ASSERT NOT ( u, t ) IS_IN z;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc b/test/regress/regress0/rels/join-eq-u-sat.cvc
new file mode 100644
index 000000000..0202cbb41
--- /dev/null
+++ b/test/regress/regress0/rels/join-eq-u-sat.cvc
@@ -0,0 +1,22 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+DATATYPE unit = u END;
+IntUPair: TYPE = [INT, unit];
+UIntPair: TYPE = [unit, INT];
+w : SET OF IntUPair;
+z : SET OF UIntPair;
+
+ASSERT  (x JOIN y) =  (w JOIN z);
+
+ASSERT (0,1) IS_IN (x JOIN y);
+ASSERT (0,u) IS_IN w;
+
+t : INT;
+ASSERT t > 0 AND t < 3;
+
+ASSERT NOT (u, t ) IS_IN z;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/join-eq-u.cvc b/test/regress/regress0/rels/join-eq-u.cvc
new file mode 100644
index 000000000..4bc498aec
--- /dev/null
+++ b/test/regress/regress0/rels/join-eq-u.cvc
@@ -0,0 +1,22 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+DATATYPE unit = u END;
+IntUPair: TYPE = [INT, unit];
+UIntPair: TYPE = [unit, INT];
+w : SET OF IntUPair;
+z : SET OF UIntPair;
+
+ASSERT  (x JOIN y) =  (w JOIN z);
+
+ASSERT (0,1) IS_IN (x JOIN y);
+ASSERT (0,u) IS_IN w;
+
+t : INT;
+ASSERT t > 0 AND t < 2;
+
+ASSERT NOT (u, t ) IS_IN z;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc
new file mode 100644
index 000000000..f39c23438
--- /dev/null
+++ b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc
@@ -0,0 +1,19 @@
+% EXPECT: sat
+OPTION "logic" "QF_UFDTFS";
+DATATYPE Atom = atom END;
+
+
+t : SET OF [Atom, Atom];
+b : Atom;
+a : Atom;
+c : Atom;
+J : ( SET OF [Atom], SET OF [Atom, Atom] ) -> SET OF [Atom];
+T : SET OF [Atom, Atom] -> SET OF [Atom, Atom];
+
+%ASSERT t = {} :: SET OF [Atom, Atom];
+
+
+ASSERT ({TUPLE(a)} JOIN t) = J({TUPLE(a)}, t);
+ASSERT NOT( ({TUPLE(c)} JOIN TCLOSURE(t)) = {TUPLE(c)} );
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/prod-mod-eq.cvc b/test/regress/regress0/rels/prod-mod-eq.cvc
new file mode 100644
index 000000000..96ef2ffba
--- /dev/null
+++ b/test/regress/regress0/rels/prod-mod-eq.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntPairPair: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPairPair;
+z1 : SET OF IntPair;
+w1 : SET OF IntPair;
+z2 : SET OF IntPair;
+w2 : SET OF IntPair;
+
+%ASSERT NOT (0,1,2,3) IS_IN (x PRODUCT y);
+
+ASSERT NOT( z = (x PRODUCT y) );
+
+ASSERT (0,1,2,3) IS_IN z;
+
+ASSERT (0,1) IS_IN z1;
+ASSERT (0,1) IS_IN z2;
+ASSERT (2,3) IS_IN w1;
+ASSERT (2,3) IS_IN w2;
+
+ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 );
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/prod-mod-eq2.cvc b/test/regress/regress0/rels/prod-mod-eq2.cvc
new file mode 100644
index 000000000..b9341a216
--- /dev/null
+++ b/test/regress/regress0/rels/prod-mod-eq2.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntPairPair: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPairPair;
+z1 : SET OF IntPair;
+w1 : SET OF IntPair;
+z2 : SET OF IntPair;
+w2 : SET OF IntPair;
+P : SET OF IntPairPair -> BOOLEAN;
+
+ASSERT z = (x PRODUCT y);
+
+ASSERT P( z );
+ASSERT NOT P( {(0,1,2,3)} );
+
+ASSERT (0,1) IS_IN z1;
+ASSERT (0,1) IS_IN z2;
+ASSERT (2,3) IS_IN w1;
+ASSERT (2,3) IS_IN w2;
+
+ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 );
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_1tup_0.cvc b/test/regress/regress0/rels/rel_1tup_0.cvc
new file mode 100644
index 000000000..50d4defd5
--- /dev/null
+++ b/test/regress/regress0/rels/rel_1tup_0.cvc
@@ -0,0 +1,24 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT];
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntTup;
+z: SET OF IntTup;
+
+b : IntPair;
+ASSERT b = (2, 1);
+ASSERT b IS_IN x;
+
+a : IntTup;
+ASSERT a = TUPLE(1);
+ASSERT a IS_IN y;
+
+c : IntTup;
+ASSERT c = TUPLE(2);
+
+ASSERT z = (x JOIN y);
+
+ASSERT NOT (c IS_IN z);
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/rel_complex_0.cvc b/test/regress/regress0/rels/rel_complex_0.cvc
new file mode 100644
index 000000000..dcb753973
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_0.cvc
@@ -0,0 +1,31 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+z : SET OF INT;
+f : INT;
+g : INT;
+
+e : IntPair;
+ASSERT e = (4, f);
+ASSERT e IS_IN x;
+
+d : IntPair;
+ASSERT d = (g,3);
+ASSERT d IS_IN y;
+
+
+ASSERT z = {f, g};
+ASSERT 0 = f - g;
+
+
+
+a : IntPair;
+ASSERT a = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_complex_1.cvc b/test/regress/regress0/rels/rel_complex_1.cvc
new file mode 100644
index 000000000..969d0d71c
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_1.cvc
@@ -0,0 +1,34 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+w : SET OF IntTup;
+z : SET OF IntTup;
+r2 : SET OF IntPair;
+
+a : IntPair;
+ASSERT a = (3,1);
+ASSERT a IS_IN x;
+
+d : IntPair;
+ASSERT d = (1,3);
+ASSERT d IS_IN y;
+
+e : IntPair;
+ASSERT e = (4,3);
+ASSERT r = (x JOIN y);
+
+ASSERT TUPLE(1) IS_IN w;
+ASSERT TUPLE(2) IS_IN z;
+ASSERT r2 = (w PRODUCT z);
+
+ASSERT NOT (e IS_IN r);
+%ASSERT e IS_IN r2;
+ASSERT (r <= r2);
+ASSERT NOT ((3,3) IS_IN r2);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_complex_3.cvc b/test/regress/regress0/rels/rel_complex_3.cvc
new file mode 100644
index 000000000..492c94432
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_3.cvc
@@ -0,0 +1,49 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+w : SET OF IntPair;
+
+
+f : IntPair;
+ASSERT f = (3,1);
+ASSERT f IS_IN x;
+
+g : IntPair;
+ASSERT g = (1,3);
+ASSERT g IS_IN y;
+
+h : IntPair;
+ASSERT h = (3,5);
+ASSERT h IS_IN x;
+ASSERT h IS_IN y;
+
+ASSERT r = (x JOIN y);
+
+e : IntPair;
+
+ASSERT NOT (e IS_IN r);
+ASSERT NOT(z = (x & y));
+ASSERT z = (x - y);
+ASSERT x <= y;
+ASSERT e IS_IN (r JOIN z);
+ASSERT e IS_IN x;
+ASSERT e IS_IN (x & y);
+CHECKSAT TRUE;
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/regress/regress0/rels/rel_complex_4.cvc b/test/regress/regress0/rels/rel_complex_4.cvc
new file mode 100644
index 000000000..f473b00aa
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_4.cvc
@@ -0,0 +1,52 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+w : SET OF IntPair;
+
+
+f : IntPair;
+ASSERT f = (3,1);
+ASSERT f IS_IN x;
+
+g : IntPair;
+ASSERT g = (1,3);
+ASSERT g IS_IN y;
+
+h : IntPair;
+ASSERT h = (3,5);
+ASSERT h IS_IN x;
+ASSERT h IS_IN y;
+
+ASSERT r = (x JOIN y);
+a:INT;
+e : IntPair;
+ASSERT e = (a,a);
+ASSERT w = {e};
+ASSERT TRANSPOSE(w) <= y;
+
+ASSERT NOT (e IS_IN r);
+ASSERT NOT(z = (x & y));
+ASSERT z = (x - y);
+ASSERT x <= y;
+ASSERT e IS_IN (r JOIN z);
+ASSERT e IS_IN x;
+ASSERT e IS_IN (x & y);
+CHECKSAT TRUE;
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/regress/regress0/rels/rel_complex_5.cvc b/test/regress/regress0/rels/rel_complex_5.cvc
new file mode 100644
index 000000000..d64817187
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_5.cvc
@@ -0,0 +1,55 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+w : SET OF IntPair;
+
+
+f : IntPair;
+ASSERT f = (3,1);
+ASSERT f IS_IN x;
+
+g : IntPair;
+ASSERT g = (1,3);
+ASSERT g IS_IN y;
+
+h : IntPair;
+ASSERT h = (3,5);
+ASSERT h IS_IN x;
+ASSERT h IS_IN y;
+
+ASSERT r = (x JOIN y);
+a:IntTup;
+ASSERT a = TUPLE(1);
+e : IntPair;
+ASSERT e = (1,1);
+
+ASSERT w = ({a} PRODUCT {a});
+ASSERT TRANSPOSE(w) <= y;
+
+ASSERT NOT (e IS_IN r);
+ASSERT NOT(z = (x & y));
+ASSERT z = (x - y);
+ASSERT x <= y;
+ASSERT e IS_IN (r JOIN z);
+ASSERT e IS_IN x;
+ASSERT e IS_IN (x & y);
+CHECKSAT TRUE;
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/regress/regress0/rels/rel_conflict_0.cvc b/test/regress/regress0/rels/rel_conflict_0.cvc
new file mode 100644
index 000000000..c1b82339f
--- /dev/null
+++ b/test/regress/regress0/rels/rel_conflict_0.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+e : IntPair;
+ASSERT e = (4, 4);
+ASSERT e IS_IN x;
+
+ASSERT NOT ((4, 4) IS_IN x);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_0.cvc b/test/regress/regress0/rels/rel_join_0.cvc
new file mode 100644
index 000000000..406b8d312
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_0.cvc
@@ -0,0 +1,24 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (7, 5) IS_IN y;
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_0_1.cvc b/test/regress/regress0/rels/rel_join_0_1.cvc
new file mode 100644
index 000000000..a7fa7efb9
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_0_1.cvc
@@ -0,0 +1,27 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (4, 3) IS_IN x;
+ASSERT (7, 5) IS_IN y;
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+%ASSERT a IS_IN (x JOIN y);
+%ASSERT NOT (v IS_IN (x JOIN y));
+ASSERT a IS_IN (x JOIN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_1.cvc b/test/regress/regress0/rels/rel_join_1.cvc
new file mode 100644
index 000000000..c8921afb9
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_1.cvc
@@ -0,0 +1,31 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+
+%ASSERT (a IS_IN (r JOIN(x JOIN y)));
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_1_1.cvc b/test/regress/regress0/rels/rel_join_1_1.cvc
new file mode 100644
index 000000000..75fc08387
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_1_1.cvc
@@ -0,0 +1,31 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+
+%ASSERT (a IS_IN (r JOIN(x JOIN y)));
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT r = (x JOIN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_2.cvc b/test/regress/regress0/rels/rel_join_2.cvc
new file mode 100644
index 000000000..cac7ce84d
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_2.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntTup;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntTup;
+ASSERT zt = (2,1,3);
+a : IntTup;
+ASSERT a = (1,1,3);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_2_1.cvc b/test/regress/regress0/rels/rel_join_2_1.cvc
new file mode 100644
index 000000000..3e27b9cc5
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_2_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntTup;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntTup;
+ASSERT zt = (2,1,3);
+a : IntTup;
+ASSERT a = (1,1,3);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+
+ASSERT a IS_IN (x JOIN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_3.cvc b/test/regress/regress0/rels/rel_join_3.cvc
new file mode 100644
index 000000000..6e190cecf
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_3.cvc
@@ -0,0 +1,29 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN r);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_3_1.cvc b/test/regress/regress0/rels/rel_join_3_1.cvc
new file mode 100644
index 000000000..dedc4ae44
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_3_1.cvc
@@ -0,0 +1,29 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT a IS_IN r;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_4.cvc b/test/regress/regress0/rels/rel_join_4.cvc
new file mode 100644
index 000000000..030810f3d
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_4.cvc
@@ -0,0 +1,32 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+b : IntPair;
+ASSERT b = (7, 5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT b IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN r);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_5.cvc b/test/regress/regress0/rels/rel_join_5.cvc
new file mode 100644
index 000000000..5209d8131
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_5.cvc
@@ -0,0 +1,19 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+ASSERT (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (1,4);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_6.cvc b/test/regress/regress0/rels/rel_join_6.cvc
new file mode 100644
index 000000000..17318872f
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_6.cvc
@@ -0,0 +1,13 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+ASSERT x = {(1,2), (3, 4)};
+
+ASSERT y = (x  JOIN {(2,1), (4,3)});
+
+ASSERT NOT ((1,1) IS_IN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_join_7.cvc b/test/regress/regress0/rels/rel_join_7.cvc
new file mode 100644
index 000000000..fff5b6efe
--- /dev/null
+++ b/test/regress/regress0/rels/rel_join_7.cvc
@@ -0,0 +1,26 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+w : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (7, 5) IS_IN y;
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT w = (r | (x JOIN y));
+ASSERT NOT (a IS_IN w);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_mix_0_1.cvc b/test/regress/regress0/rels/rel_mix_0_1.cvc
new file mode 100644
index 000000000..723a9b2e2
--- /dev/null
+++ b/test/regress/regress0/rels/rel_mix_0_1.cvc
@@ -0,0 +1,30 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+w : SET OF IntTup;
+z : SET OF IntTup;
+r2 : SET OF IntPair;
+
+d : IntPair;
+ASSERT d = (1,3);
+ASSERT (1,3) IS_IN y;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+
+ASSERT r = (x JOIN y);
+ASSERT r2 = (w PRODUCT z);
+
+ASSERT NOT (e IS_IN r);
+%ASSERT e IS_IN r2;
+ASSERT NOT (r = r2);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_pressure_0.cvc b/test/regress/regress0/rels/rel_pressure_0.cvc
new file mode 100644
index 000000000..6cdf03600
--- /dev/null
+++ b/test/regress/regress0/rels/rel_pressure_0.cvc
@@ -0,0 +1,617 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+a11 : IntPair;
+ASSERT a11 = (1, 1);
+ASSERT a11 IS_IN x;
+a12 : IntPair;
+ASSERT a12 = (1, 2);
+ASSERT a12 IS_IN x;
+a13 : IntPair;
+ASSERT a13 = (1, 3);
+ASSERT a13 IS_IN x;
+a14 : IntPair;
+ASSERT a14 = (1, 4);
+ASSERT a14 IS_IN x;
+a15 : IntPair;
+ASSERT a15 = (1, 5);
+ASSERT a15 IS_IN x;
+a16 : IntPair;
+ASSERT a16 = (1, 6);
+ASSERT a16 IS_IN x;
+a17 : IntPair;
+ASSERT a17 = (1, 7);
+ASSERT a17 IS_IN x;
+a18 : IntPair;
+ASSERT a18 = (1, 8);
+ASSERT a18 IS_IN x;
+a19 : IntPair;
+ASSERT a19 = (1, 9);
+ASSERT a19 IS_IN x;
+a110 : IntPair;
+ASSERT a110 = (1, 10);
+ASSERT a110 IS_IN x;
+a21 : IntPair;
+ASSERT a21 = (2, 1);
+ASSERT a21 IS_IN x;
+a22 : IntPair;
+ASSERT a22 = (2, 2);
+ASSERT a22 IS_IN x;
+a23 : IntPair;
+ASSERT a23 = (2, 3);
+ASSERT a23 IS_IN x;
+a24 : IntPair;
+ASSERT a24 = (2, 4);
+ASSERT a24 IS_IN x;
+a25 : IntPair;
+ASSERT a25 = (2, 5);
+ASSERT a25 IS_IN x;
+a26 : IntPair;
+ASSERT a26 = (2, 6);
+ASSERT a26 IS_IN x;
+a27 : IntPair;
+ASSERT a27 = (2, 7);
+ASSERT a27 IS_IN x;
+a28 : IntPair;
+ASSERT a28 = (2, 8);
+ASSERT a28 IS_IN x;
+a29 : IntPair;
+ASSERT a29 = (2, 9);
+ASSERT a29 IS_IN x;
+a210 : IntPair;
+ASSERT a210 = (2, 10);
+ASSERT a210 IS_IN x;
+a31 : IntPair;
+ASSERT a31 = (3, 1);
+ASSERT a31 IS_IN x;
+a32 : IntPair;
+ASSERT a32 = (3, 2);
+ASSERT a32 IS_IN x;
+a33 : IntPair;
+ASSERT a33 = (3, 3);
+ASSERT a33 IS_IN x;
+a34 : IntPair;
+ASSERT a34 = (3, 4);
+ASSERT a34 IS_IN x;
+a35 : IntPair;
+ASSERT a35 = (3, 5);
+ASSERT a35 IS_IN x;
+a36 : IntPair;
+ASSERT a36 = (3, 6);
+ASSERT a36 IS_IN x;
+a37 : IntPair;
+ASSERT a37 = (3, 7);
+ASSERT a37 IS_IN x;
+a38 : IntPair;
+ASSERT a38 = (3, 8);
+ASSERT a38 IS_IN x;
+a39 : IntPair;
+ASSERT a39 = (3, 9);
+ASSERT a39 IS_IN x;
+a310 : IntPair;
+ASSERT a310 = (3, 10);
+ASSERT a310 IS_IN x;
+a41 : IntPair;
+ASSERT a41 = (4, 1);
+ASSERT a41 IS_IN x;
+a42 : IntPair;
+ASSERT a42 = (4, 2);
+ASSERT a42 IS_IN x;
+a43 : IntPair;
+ASSERT a43 = (4, 3);
+ASSERT a43 IS_IN x;
+a44 : IntPair;
+ASSERT a44 = (4, 4);
+ASSERT a44 IS_IN x;
+a45 : IntPair;
+ASSERT a45 = (4, 5);
+ASSERT a45 IS_IN x;
+a46 : IntPair;
+ASSERT a46 = (4, 6);
+ASSERT a46 IS_IN x;
+a47 : IntPair;
+ASSERT a47 = (4, 7);
+ASSERT a47 IS_IN x;
+a48 : IntPair;
+ASSERT a48 = (4, 8);
+ASSERT a48 IS_IN x;
+a49 : IntPair;
+ASSERT a49 = (4, 9);
+ASSERT a49 IS_IN x;
+a410 : IntPair;
+ASSERT a410 = (4, 10);
+ASSERT a410 IS_IN x;
+a51 : IntPair;
+ASSERT a51 = (5, 1);
+ASSERT a51 IS_IN x;
+a52 : IntPair;
+ASSERT a52 = (5, 2);
+ASSERT a52 IS_IN x;
+a53 : IntPair;
+ASSERT a53 = (5, 3);
+ASSERT a53 IS_IN x;
+a54 : IntPair;
+ASSERT a54 = (5, 4);
+ASSERT a54 IS_IN x;
+a55 : IntPair;
+ASSERT a55 = (5, 5);
+ASSERT a55 IS_IN x;
+a56 : IntPair;
+ASSERT a56 = (5, 6);
+ASSERT a56 IS_IN x;
+a57 : IntPair;
+ASSERT a57 = (5, 7);
+ASSERT a57 IS_IN x;
+a58 : IntPair;
+ASSERT a58 = (5, 8);
+ASSERT a58 IS_IN x;
+a59 : IntPair;
+ASSERT a59 = (5, 9);
+ASSERT a59 IS_IN x;
+a510 : IntPair;
+ASSERT a510 = (5, 10);
+ASSERT a510 IS_IN x;
+a61 : IntPair;
+ASSERT a61 = (6, 1);
+ASSERT a61 IS_IN x;
+a62 : IntPair;
+ASSERT a62 = (6, 2);
+ASSERT a62 IS_IN x;
+a63 : IntPair;
+ASSERT a63 = (6, 3);
+ASSERT a63 IS_IN x;
+a64 : IntPair;
+ASSERT a64 = (6, 4);
+ASSERT a64 IS_IN x;
+a65 : IntPair;
+ASSERT a65 = (6, 5);
+ASSERT a65 IS_IN x;
+a66 : IntPair;
+ASSERT a66 = (6, 6);
+ASSERT a66 IS_IN x;
+a67 : IntPair;
+ASSERT a67 = (6, 7);
+ASSERT a67 IS_IN x;
+a68 : IntPair;
+ASSERT a68 = (6, 8);
+ASSERT a68 IS_IN x;
+a69 : IntPair;
+ASSERT a69 = (6, 9);
+ASSERT a69 IS_IN x;
+a610 : IntPair;
+ASSERT a610 = (6, 10);
+ASSERT a610 IS_IN x;
+a71 : IntPair;
+ASSERT a71 = (7, 1);
+ASSERT a71 IS_IN x;
+a72 : IntPair;
+ASSERT a72 = (7, 2);
+ASSERT a72 IS_IN x;
+a73 : IntPair;
+ASSERT a73 = (7, 3);
+ASSERT a73 IS_IN x;
+a74 : IntPair;
+ASSERT a74 = (7, 4);
+ASSERT a74 IS_IN x;
+a75 : IntPair;
+ASSERT a75 = (7, 5);
+ASSERT a75 IS_IN x;
+a76 : IntPair;
+ASSERT a76 = (7, 6);
+ASSERT a76 IS_IN x;
+a77 : IntPair;
+ASSERT a77 = (7, 7);
+ASSERT a77 IS_IN x;
+a78 : IntPair;
+ASSERT a78 = (7, 8);
+ASSERT a78 IS_IN x;
+a79 : IntPair;
+ASSERT a79 = (7, 9);
+ASSERT a79 IS_IN x;
+a710 : IntPair;
+ASSERT a710 = (7, 10);
+ASSERT a710 IS_IN x;
+a81 : IntPair;
+ASSERT a81 = (8, 1);
+ASSERT a81 IS_IN x;
+a82 : IntPair;
+ASSERT a82 = (8, 2);
+ASSERT a82 IS_IN x;
+a83 : IntPair;
+ASSERT a83 = (8, 3);
+ASSERT a83 IS_IN x;
+a84 : IntPair;
+ASSERT a84 = (8, 4);
+ASSERT a84 IS_IN x;
+a85 : IntPair;
+ASSERT a85 = (8, 5);
+ASSERT a85 IS_IN x;
+a86 : IntPair;
+ASSERT a86 = (8, 6);
+ASSERT a86 IS_IN x;
+a87 : IntPair;
+ASSERT a87 = (8, 7);
+ASSERT a87 IS_IN x;
+a88 : IntPair;
+ASSERT a88 = (8, 8);
+ASSERT a88 IS_IN x;
+a89 : IntPair;
+ASSERT a89 = (8, 9);
+ASSERT a89 IS_IN x;
+a810 : IntPair;
+ASSERT a810 = (8, 10);
+ASSERT a810 IS_IN x;
+a91 : IntPair;
+ASSERT a91 = (9, 1);
+ASSERT a91 IS_IN x;
+a92 : IntPair;
+ASSERT a92 = (9, 2);
+ASSERT a92 IS_IN x;
+a93 : IntPair;
+ASSERT a93 = (9, 3);
+ASSERT a93 IS_IN x;
+a94 : IntPair;
+ASSERT a94 = (9, 4);
+ASSERT a94 IS_IN x;
+a95 : IntPair;
+ASSERT a95 = (9, 5);
+ASSERT a95 IS_IN x;
+a96 : IntPair;
+ASSERT a96 = (9, 6);
+ASSERT a96 IS_IN x;
+a97 : IntPair;
+ASSERT a97 = (9, 7);
+ASSERT a97 IS_IN x;
+a98 : IntPair;
+ASSERT a98 = (9, 8);
+ASSERT a98 IS_IN x;
+a99 : IntPair;
+ASSERT a99 = (9, 9);
+ASSERT a99 IS_IN x;
+a910 : IntPair;
+ASSERT a910 = (9, 10);
+ASSERT a910 IS_IN x;
+a101 : IntPair;
+ASSERT a101 = (10, 1);
+ASSERT a101 IS_IN x;
+a102 : IntPair;
+ASSERT a102 = (10, 2);
+ASSERT a102 IS_IN x;
+a103 : IntPair;
+ASSERT a103 = (10, 3);
+ASSERT a103 IS_IN x;
+a104 : IntPair;
+ASSERT a104 = (10, 4);
+ASSERT a104 IS_IN x;
+a105 : IntPair;
+ASSERT a105 = (10, 5);
+ASSERT a105 IS_IN x;
+a106 : IntPair;
+ASSERT a106 = (10, 6);
+ASSERT a106 IS_IN x;
+a107 : IntPair;
+ASSERT a107 = (10, 7);
+ASSERT a107 IS_IN x;
+a108 : IntPair;
+ASSERT a108 = (10, 8);
+ASSERT a108 IS_IN x;
+a109 : IntPair;
+ASSERT a109 = (10, 9);
+ASSERT a109 IS_IN x;
+a1010 : IntPair;
+ASSERT a1010 = (10, 10);
+ASSERT a1010 IS_IN x;
+b11 : IntPair;
+ASSERT b11 = (1, 1);
+ASSERT b11 IS_IN y;
+b12 : IntPair;
+ASSERT b12 = (1, 2);
+ASSERT b12 IS_IN y;
+b13 : IntPair;
+ASSERT b13 = (1, 3);
+ASSERT b13 IS_IN y;
+b14 : IntPair;
+ASSERT b14 = (1, 4);
+ASSERT b14 IS_IN y;
+b15 : IntPair;
+ASSERT b15 = (1, 5);
+ASSERT b15 IS_IN y;
+b16 : IntPair;
+ASSERT b16 = (1, 6);
+ASSERT b16 IS_IN y;
+b17 : IntPair;
+ASSERT b17 = (1, 7);
+ASSERT b17 IS_IN y;
+b18 : IntPair;
+ASSERT b18 = (1, 8);
+ASSERT b18 IS_IN y;
+b19 : IntPair;
+ASSERT b19 = (1, 9);
+ASSERT b19 IS_IN y;
+b110 : IntPair;
+ASSERT b110 = (1, 10);
+ASSERT b110 IS_IN y;
+b21 : IntPair;
+ASSERT b21 = (2, 1);
+ASSERT b21 IS_IN y;
+b22 : IntPair;
+ASSERT b22 = (2, 2);
+ASSERT b22 IS_IN y;
+b23 : IntPair;
+ASSERT b23 = (2, 3);
+ASSERT b23 IS_IN y;
+b24 : IntPair;
+ASSERT b24 = (2, 4);
+ASSERT b24 IS_IN y;
+b25 : IntPair;
+ASSERT b25 = (2, 5);
+ASSERT b25 IS_IN y;
+b26 : IntPair;
+ASSERT b26 = (2, 6);
+ASSERT b26 IS_IN y;
+b27 : IntPair;
+ASSERT b27 = (2, 7);
+ASSERT b27 IS_IN y;
+b28 : IntPair;
+ASSERT b28 = (2, 8);
+ASSERT b28 IS_IN y;
+b29 : IntPair;
+ASSERT b29 = (2, 9);
+ASSERT b29 IS_IN y;
+b210 : IntPair;
+ASSERT b210 = (2, 10);
+ASSERT b210 IS_IN y;
+b31 : IntPair;
+ASSERT b31 = (3, 1);
+ASSERT b31 IS_IN y;
+b32 : IntPair;
+ASSERT b32 = (3, 2);
+ASSERT b32 IS_IN y;
+b33 : IntPair;
+ASSERT b33 = (3, 3);
+ASSERT b33 IS_IN y;
+b34 : IntPair;
+ASSERT b34 = (3, 4);
+ASSERT b34 IS_IN y;
+b35 : IntPair;
+ASSERT b35 = (3, 5);
+ASSERT b35 IS_IN y;
+b36 : IntPair;
+ASSERT b36 = (3, 6);
+ASSERT b36 IS_IN y;
+b37 : IntPair;
+ASSERT b37 = (3, 7);
+ASSERT b37 IS_IN y;
+b38 : IntPair;
+ASSERT b38 = (3, 8);
+ASSERT b38 IS_IN y;
+b39 : IntPair;
+ASSERT b39 = (3, 9);
+ASSERT b39 IS_IN y;
+b310 : IntPair;
+ASSERT b310 = (3, 10);
+ASSERT b310 IS_IN y;
+b41 : IntPair;
+ASSERT b41 = (4, 1);
+ASSERT b41 IS_IN y;
+b42 : IntPair;
+ASSERT b42 = (4, 2);
+ASSERT b42 IS_IN y;
+b43 : IntPair;
+ASSERT b43 = (4, 3);
+ASSERT b43 IS_IN y;
+b44 : IntPair;
+ASSERT b44 = (4, 4);
+ASSERT b44 IS_IN y;
+b45 : IntPair;
+ASSERT b45 = (4, 5);
+ASSERT b45 IS_IN y;
+b46 : IntPair;
+ASSERT b46 = (4, 6);
+ASSERT b46 IS_IN y;
+b47 : IntPair;
+ASSERT b47 = (4, 7);
+ASSERT b47 IS_IN y;
+b48 : IntPair;
+ASSERT b48 = (4, 8);
+ASSERT b48 IS_IN y;
+b49 : IntPair;
+ASSERT b49 = (4, 9);
+ASSERT b49 IS_IN y;
+b410 : IntPair;
+ASSERT b410 = (4, 10);
+ASSERT b410 IS_IN y;
+b51 : IntPair;
+ASSERT b51 = (5, 1);
+ASSERT b51 IS_IN y;
+b52 : IntPair;
+ASSERT b52 = (5, 2);
+ASSERT b52 IS_IN y;
+b53 : IntPair;
+ASSERT b53 = (5, 3);
+ASSERT b53 IS_IN y;
+b54 : IntPair;
+ASSERT b54 = (5, 4);
+ASSERT b54 IS_IN y;
+b55 : IntPair;
+ASSERT b55 = (5, 5);
+ASSERT b55 IS_IN y;
+b56 : IntPair;
+ASSERT b56 = (5, 6);
+ASSERT b56 IS_IN y;
+b57 : IntPair;
+ASSERT b57 = (5, 7);
+ASSERT b57 IS_IN y;
+b58 : IntPair;
+ASSERT b58 = (5, 8);
+ASSERT b58 IS_IN y;
+b59 : IntPair;
+ASSERT b59 = (5, 9);
+ASSERT b59 IS_IN y;
+b510 : IntPair;
+ASSERT b510 = (5, 10);
+ASSERT b510 IS_IN y;
+b61 : IntPair;
+ASSERT b61 = (6, 1);
+ASSERT b61 IS_IN y;
+b62 : IntPair;
+ASSERT b62 = (6, 2);
+ASSERT b62 IS_IN y;
+b63 : IntPair;
+ASSERT b63 = (6, 3);
+ASSERT b63 IS_IN y;
+b64 : IntPair;
+ASSERT b64 = (6, 4);
+ASSERT b64 IS_IN y;
+b65 : IntPair;
+ASSERT b65 = (6, 5);
+ASSERT b65 IS_IN y;
+b66 : IntPair;
+ASSERT b66 = (6, 6);
+ASSERT b66 IS_IN y;
+b67 : IntPair;
+ASSERT b67 = (6, 7);
+ASSERT b67 IS_IN y;
+b68 : IntPair;
+ASSERT b68 = (6, 8);
+ASSERT b68 IS_IN y;
+b69 : IntPair;
+ASSERT b69 = (6, 9);
+ASSERT b69 IS_IN y;
+b610 : IntPair;
+ASSERT b610 = (6, 10);
+ASSERT b610 IS_IN y;
+b71 : IntPair;
+ASSERT b71 = (7, 1);
+ASSERT b71 IS_IN y;
+b72 : IntPair;
+ASSERT b72 = (7, 2);
+ASSERT b72 IS_IN y;
+b73 : IntPair;
+ASSERT b73 = (7, 3);
+ASSERT b73 IS_IN y;
+b74 : IntPair;
+ASSERT b74 = (7, 4);
+ASSERT b74 IS_IN y;
+b75 : IntPair;
+ASSERT b75 = (7, 5);
+ASSERT b75 IS_IN y;
+b76 : IntPair;
+ASSERT b76 = (7, 6);
+ASSERT b76 IS_IN y;
+b77 : IntPair;
+ASSERT b77 = (7, 7);
+ASSERT b77 IS_IN y;
+b78 : IntPair;
+ASSERT b78 = (7, 8);
+ASSERT b78 IS_IN y;
+b79 : IntPair;
+ASSERT b79 = (7, 9);
+ASSERT b79 IS_IN y;
+b710 : IntPair;
+ASSERT b710 = (7, 10);
+ASSERT b710 IS_IN y;
+b81 : IntPair;
+ASSERT b81 = (8, 1);
+ASSERT b81 IS_IN y;
+b82 : IntPair;
+ASSERT b82 = (8, 2);
+ASSERT b82 IS_IN y;
+b83 : IntPair;
+ASSERT b83 = (8, 3);
+ASSERT b83 IS_IN y;
+b84 : IntPair;
+ASSERT b84 = (8, 4);
+ASSERT b84 IS_IN y;
+b85 : IntPair;
+ASSERT b85 = (8, 5);
+ASSERT b85 IS_IN y;
+b86 : IntPair;
+ASSERT b86 = (8, 6);
+ASSERT b86 IS_IN y;
+b87 : IntPair;
+ASSERT b87 = (8, 7);
+ASSERT b87 IS_IN y;
+b88 : IntPair;
+ASSERT b88 = (8, 8);
+ASSERT b88 IS_IN y;
+b89 : IntPair;
+ASSERT b89 = (8, 9);
+ASSERT b89 IS_IN y;
+b810 : IntPair;
+ASSERT b810 = (8, 10);
+ASSERT b810 IS_IN y;
+b91 : IntPair;
+ASSERT b91 = (9, 1);
+ASSERT b91 IS_IN y;
+b92 : IntPair;
+ASSERT b92 = (9, 2);
+ASSERT b92 IS_IN y;
+b93 : IntPair;
+ASSERT b93 = (9, 3);
+ASSERT b93 IS_IN y;
+b94 : IntPair;
+ASSERT b94 = (9, 4);
+ASSERT b94 IS_IN y;
+b95 : IntPair;
+ASSERT b95 = (9, 5);
+ASSERT b95 IS_IN y;
+b96 : IntPair;
+ASSERT b96 = (9, 6);
+ASSERT b96 IS_IN y;
+b97 : IntPair;
+ASSERT b97 = (9, 7);
+ASSERT b97 IS_IN y;
+b98 : IntPair;
+ASSERT b98 = (9, 8);
+ASSERT b98 IS_IN y;
+b99 : IntPair;
+ASSERT b99 = (9, 9);
+ASSERT b99 IS_IN y;
+b910 : IntPair;
+ASSERT b910 = (9, 10);
+ASSERT b910 IS_IN y;
+b101 : IntPair;
+ASSERT b101 = (10, 1);
+ASSERT b101 IS_IN y;
+b102 : IntPair;
+ASSERT b102 = (10, 2);
+ASSERT b102 IS_IN y;
+b103 : IntPair;
+ASSERT b103 = (10, 3);
+ASSERT b103 IS_IN y;
+b104 : IntPair;
+ASSERT b104 = (10, 4);
+ASSERT b104 IS_IN y;
+b105 : IntPair;
+ASSERT b105 = (10, 5);
+ASSERT b105 IS_IN y;
+b106 : IntPair;
+ASSERT b106 = (10, 6);
+ASSERT b106 IS_IN y;
+b107 : IntPair;
+ASSERT b107 = (10, 7);
+ASSERT b107 IS_IN y;
+b108 : IntPair;
+ASSERT b108 = (10, 8);
+ASSERT b108 IS_IN y;
+b109 : IntPair;
+ASSERT b109 = (10, 9);
+ASSERT b109 IS_IN y;
+b1010 : IntPair;
+ASSERT b1010 = (10, 10);
+ASSERT b1010 IS_IN y;
+
+ASSERT (1, 9) IS_IN z;
+
+a : IntPair;
+ASSERT a = (9,1);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_product_0.cvc b/test/regress/regress0/rels/rel_product_0.cvc
new file mode 100644
index 000000000..09981be0b
--- /dev/null
+++ b/test/regress/regress0/rels/rel_product_0.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (v IS_IN (x PRODUCT y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_product_0_1.cvc b/test/regress/regress0/rels/rel_product_0_1.cvc
new file mode 100644
index 000000000..f141c7bd4
--- /dev/null
+++ b/test/regress/regress0/rels/rel_product_0_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT v IS_IN (x PRODUCT y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_product_1.cvc b/test/regress/regress0/rels/rel_product_1.cvc
new file mode 100644
index 000000000..1826e5a75
--- /dev/null
+++ b/test/regress/regress0/rels/rel_product_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2,3);
+zt : IntPair;
+ASSERT zt = (3,2,1);
+v : IntTup;
+ASSERT v = (1,2,3,3,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (v IS_IN (x PRODUCT y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_product_1_1.cvc b/test/regress/regress0/rels/rel_product_1_1.cvc
new file mode 100644
index 000000000..2d79cbc0c
--- /dev/null
+++ b/test/regress/regress0/rels/rel_product_1_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntTup;
+
+z : IntPair;
+ASSERT z = (1,2,3);
+zt : IntPair;
+ASSERT zt = (3,2,1);
+
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT (1,1,1,1,1,1) IS_IN r;
+ASSERT r = (x PRODUCT y);
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_symbolic_1.cvc b/test/regress/regress0/rels/rel_symbolic_1.cvc
new file mode 100644
index 000000000..08ed32411
--- /dev/null
+++ b/test/regress/regress0/rels/rel_symbolic_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+f : INT;
+d : IntPair;
+ASSERT d = (f,3);
+ASSERT d IS_IN y;
+e : IntPair;
+ASSERT e = (4, f);
+ASSERT e IS_IN x;
+
+a : IntPair;
+ASSERT a = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/rels/rel_symbolic_1_1.cvc
new file mode 100644
index 000000000..df2d7f412
--- /dev/null
+++ b/test/regress/regress0/rels/rel_symbolic_1_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+d : IntPair;
+ASSERT d IS_IN y;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (e IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_symbolic_2_1.cvc b/test/regress/regress0/rels/rel_symbolic_2_1.cvc
new file mode 100644
index 000000000..082604dc2
--- /dev/null
+++ b/test/regress/regress0/rels/rel_symbolic_2_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+d : IntPair;
+ASSERT d = (1,3);
+ASSERT (1,3) IS_IN y;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (e IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_symbolic_3_1.cvc b/test/regress/regress0/rels/rel_symbolic_3_1.cvc
new file mode 100644
index 000000000..da0906dd2
--- /dev/null
+++ b/test/regress/regress0/rels/rel_symbolic_3_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+f : INT;
+d : IntPair;
+ASSERT d IS_IN y;
+
+e : IntPair;
+ASSERT e = (4, f);
+ASSERT e IS_IN x;
+
+a : IntPair;
+ASSERT a = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_10_1.cvc b/test/regress/regress0/rels/rel_tc_10_1.cvc
new file mode 100644
index 000000000..67c444070
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_10_1.cvc
@@ -0,0 +1,18 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+a: INT;
+b:INT;
+c:INT;
+d:INT;
+ASSERT a = c;
+ASSERT a = d;
+ASSERT (1, c) IS_IN x;
+ASSERT (2, d) IS_IN x;
+ASSERT (a, 5) IS_IN y;
+ASSERT y = (TCLOSURE x);
+ASSERT ((2, 5) IS_IN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_11.cvc b/test/regress/regress0/rels/rel_tc_11.cvc
new file mode 100644
index 000000000..7edeb0efb
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_11.cvc
@@ -0,0 +1,18 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntTup;
+ASSERT (2, 3) IS_IN x;
+ASSERT (5, 3) IS_IN x;
+ASSERT (3, 9) IS_IN x;
+ASSERT z = (x PRODUCT y);
+ASSERT (1, 2, 3, 4) IS_IN z;
+ASSERT NOT ((5, 9) IS_IN x);
+ASSERT (3, 8) IS_IN y;
+ASSERT y = (TCLOSURE x);
+ASSERT NOT ((1, 2) IS_IN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_2_1.cvc b/test/regress/regress0/rels/rel_tc_2_1.cvc
new file mode 100644
index 000000000..d5d42eaad
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_2_1.cvc
@@ -0,0 +1,28 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+ e: INT;
+
+a : IntPair;
+ASSERT a = (1,	e);
+
+d : IntPair;
+ASSERT d = (e,5);
+
+ASSERT a IS_IN x;
+ASSERT d IS_IN x;
+ASSERT NOT ((1,1) IS_IN x);
+ASSERT NOT ((1,2) IS_IN x);
+ASSERT NOT ((1,3) IS_IN x);
+ASSERT NOT ((1,4) IS_IN x);
+ASSERT NOT ((1,5) IS_IN x);
+ASSERT NOT ((1,6) IS_IN x);
+ASSERT NOT ((1,7) IS_IN x);
+
+ASSERT y = TCLOSURE(x);
+
+ASSERT (1, 5) IS_IN y;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_3.cvc b/test/regress/regress0/rels/rel_tc_3.cvc
new file mode 100644
index 000000000..39564c4cf
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_3.cvc
@@ -0,0 +1,22 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+a: INT;
+b:INT;
+c:INT;
+d:INT;
+ASSERT (1, a) IS_IN x;
+ASSERT (1, c) IS_IN x;
+ASSERT (1, d) IS_IN x;
+ASSERT (b, 1) IS_IN x;
+ASSERT (b = d);
+ASSERT (b > (d -1));
+ASSERT (b < (d+1));
+%ASSERT (2,3) IS_IN ((x JOIN x) JOIN x);
+%ASSERT NOT (2, 3) IS_IN (TCLOSURE x);
+ASSERT y = (TCLOSURE x);
+ASSERT NOT ((1, 1) IS_IN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_3_1.cvc b/test/regress/regress0/rels/rel_tc_3_1.cvc
new file mode 100644
index 000000000..7f5535656
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_3_1.cvc
@@ -0,0 +1,18 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+a: INT;
+b:INT;
+c:INT;
+d:INT;
+ASSERT (1, a) IS_IN x;
+ASSERT (1, c) IS_IN x;
+ASSERT (1, d) IS_IN x;
+ASSERT (b, 1) IS_IN x;
+ASSERT (b = d);
+
+ASSERT y = (TCLOSURE x);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_4.cvc b/test/regress/regress0/rels/rel_tc_4.cvc
new file mode 100644
index 000000000..decd38fe1
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_4.cvc
@@ -0,0 +1,19 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+a: INT;
+b:INT;
+c:INT;
+d:INT;
+ASSERT (1, a) IS_IN x;
+ASSERT (1, c) IS_IN x;
+ASSERT (1, d) IS_IN x;
+ASSERT (b, 1) IS_IN x;
+ASSERT (b = d);
+ASSERT (2,b) IS_IN ((x JOIN x) JOIN x);
+ASSERT NOT (2, 1) IS_IN (TCLOSURE x);
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_4_1.cvc b/test/regress/regress0/rels/rel_tc_4_1.cvc
new file mode 100644
index 000000000..8ee75f7e9
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_4_1.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+ASSERT y = ((TCLOSURE x) JOIN x);
+ASSERT NOT (y = TCLOSURE x);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_5_1.cvc b/test/regress/regress0/rels/rel_tc_5_1.cvc
new file mode 100644
index 000000000..fd9caeade
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_5_1.cvc
@@ -0,0 +1,9 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+ASSERT y = (TCLOSURE x);
+ASSERT NOT ( y = ((x JOIN x) JOIN x));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_6.cvc b/test/regress/regress0/rels/rel_tc_6.cvc
new file mode 100644
index 000000000..4570c5a8d
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_6.cvc
@@ -0,0 +1,9 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+ASSERT y = (TCLOSURE x);
+ASSERT NOT (((x JOIN x) JOIN x) <= y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_7.cvc b/test/regress/regress0/rels/rel_tc_7.cvc
new file mode 100644
index 000000000..15c0510a6
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_7.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+ASSERT y = ((TCLOSURE x) JOIN x);
+ASSERT (1,2) IS_IN ((x JOIN x) JOIN x);
+ASSERT NOT (y <= TCLOSURE x);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_8.cvc b/test/regress/regress0/rels/rel_tc_8.cvc
new file mode 100644
index 000000000..9f5879c6d
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_8.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+ASSERT (2, 2) IS_IN (TCLOSURE x);
+ASSERT x = {}::SET OF IntPair;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_9_1.cvc b/test/regress/regress0/rels/rel_tc_9_1.cvc
new file mode 100644
index 000000000..f884349b1
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_9_1.cvc
@@ -0,0 +1,23 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+w : SET OF IntPair;
+
+ASSERT z = (TCLOSURE x);
+ASSERT w = (x JOIN y);
+ASSERT (2, 2) IS_IN z;
+ASSERT (0,3) IS_IN y;
+ASSERT (-1,3) IS_IN y;
+ASSERT (1,3) IS_IN y;
+ASSERT (-2,3) IS_IN y;
+ASSERT (2,3) IS_IN y;
+ASSERT (3,3) IS_IN y;
+ASSERT (4,3) IS_IN y;
+ASSERT (5,3) IS_IN y;
+ASSERT NOT (2, 3) IS_IN (x JOIN y);
+ASSERT NOT (2,1) IS_IN x;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_2.cvc b/test/regress/regress0/rels/rel_tp_2.cvc
new file mode 100644
index 000000000..441e79c45
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_2.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+ASSERT (z = TRANSPOSE(y) OR z = TRANSPOSE(x));
+ASSERT NOT (TRANSPOSE(z) = y);
+ASSERT NOT (TRANSPOSE(z) = x);
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/rel_tp_3_1.cvc b/test/regress/regress0/rels/rel_tp_3_1.cvc
new file mode 100644
index 000000000..46806b432
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_3_1.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z: SET OF IntPair;
+
+ASSERT (1, 3) IS_IN x;
+ASSERT ((2,3) IS_IN z OR (2,1) IS_IN z);
+ASSERT y = (TRANSPOSE x);
+ASSERT NOT (1,2) IS_IN y;
+
+ASSERT x = z;
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/rels/rel_tp_join_0.cvc b/test/regress/regress0/rels/rel_tp_join_0.cvc
new file mode 100644
index 000000000..a03f0e3fd
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_0.cvc
@@ -0,0 +1,32 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (5,1);
+
+b : IntPair;
+ASSERT b = (7, 5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT b IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_1.cvc b/test/regress/regress0/rels/rel_tp_join_1.cvc
new file mode 100644
index 000000000..60b6edf58
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_1.cvc
@@ -0,0 +1,32 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+b : IntPair;
+ASSERT b = (1,7);
+c : IntPair;
+ASSERT c = (2,3);
+ASSERT b IS_IN x;
+ASSERT c IS_IN x;
+
+d : IntPair;
+ASSERT d = (7,3);
+e : IntPair;
+ASSERT e = (4,7);
+
+ASSERT d IS_IN y;
+ASSERT e IS_IN y;
+
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = ((x JOIN y) JOIN z);
+
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_2.cvc b/test/regress/regress0/rels/rel_tp_join_2.cvc
new file mode 100644
index 000000000..cc851f622
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_2.cvc
@@ -0,0 +1,19 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+ASSERT (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,1);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_2_1.cvc b/test/regress/regress0/rels/rel_tp_join_2_1.cvc
new file mode 100644
index 000000000..acf3dbccf
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_2_1.cvc
@@ -0,0 +1,19 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+ASSERT (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT a IS_IN (TRANSPOSE r);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_3.cvc b/test/regress/regress0/rels/rel_tp_join_3.cvc
new file mode 100644
index 000000000..25277f43a
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_3.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+% crash on this
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+ASSERT (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+ASSERT (3, 3) IS_IN w;
+
+a : IntPair;
+ASSERT a = (4,1);
+%ASSERT r = (((TRANSPOSE x) JOIN y) JOIN (w JOIN z));
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+
+zz : SET OF IntPair;
+ASSERT zz = ((TRANSPOSE x) JOIN y);
+ASSERT NOT ((1,3) IS_IN w);
+ASSERT NOT ((1,3) IS_IN (w | zz) );
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc
new file mode 100644
index 000000000..54e16dd51
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+
+ASSERT x = {(1,7), (2,3)};
+
+d : IntPair;
+ASSERT d = (7,3);
+e : IntPair;
+ASSERT e = (4,7);
+
+ASSERT d IS_IN y;
+ASSERT e IS_IN y;
+
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = ((x JOIN y) JOIN z);
+
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_int_0.cvc b/test/regress/regress0/rels/rel_tp_join_int_0.cvc
new file mode 100644
index 000000000..8d149a48d
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_int_0.cvc
@@ -0,0 +1,26 @@
+% EXPECT: unsat
+% crash on this
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+t : INT;
+u : INT;
+
+ASSERT 4 < t AND t < 6;
+ASSERT 4 < u AND u < 6;
+
+ASSERT (1, u) IS_IN x;
+ASSERT (t, 3) IS_IN y;
+
+a : IntPair;
+ASSERT a = (1,3);
+
+ASSERT NOT (a IS_IN  (x JOIN y));
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc
new file mode 100644
index 000000000..b05026bc9
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntTup;
+
+ASSERT (2, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (2, 2) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+v : IntTup;
+ASSERT v = (4,3,2,1);
+
+ASSERT r = (((TRANSPOSE x) JOIN y) PRODUCT z);
+ASSERT NOT (v IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_var_0.cvc b/test/regress/regress0/rels/rel_tp_join_var_0.cvc
new file mode 100644
index 000000000..aacf6c054
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tp_join_var_0.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+t : INT;
+u : INT;
+
+ASSERT 4 < t AND t < 6;
+ASSERT 4 < u AND u < 6;
+
+ASSERT (1, t) IS_IN x;
+ASSERT (u, 3) IS_IN y;
+
+a : IntPair;
+ASSERT a = (1,3);
+
+ASSERT NOT (a IS_IN  (x JOIN y));
+
+st : SET OF INT;
+su : SET OF INT;
+ASSERT t IS_IN st;
+ASSERT u IS_IN su;
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_0.cvc b/test/regress/regress0/rels/rel_transpose_0.cvc
new file mode 100644
index 000000000..49fb87569
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_0.cvc
@@ -0,0 +1,18 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+a: INT;
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+
+ASSERT y = (TRANSPOSE x);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc b/test/regress/regress0/rels/rel_transpose_1.cvc
new file mode 100644
index 000000000..bdcf31bb8
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_1.cvc
@@ -0,0 +1,12 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntTup;
+y : SET OF IntTup;
+z : IntTup;
+ASSERT z = (1,2,3);
+zt : IntTup;
+ASSERT zt = (3,2,1);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_1_1.cvc b/test/regress/regress0/rels/rel_transpose_1_1.cvc
new file mode 100644
index 000000000..fa6ee5069
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntTup;
+y : SET OF IntTup;
+z : IntTup;
+a: INT;
+ASSERT z = (1,2,a);
+zt : IntTup;
+ASSERT zt = (3,2,2);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN (TRANSPOSE x);
+ASSERT y = (TRANSPOSE x);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_3.cvc b/test/regress/regress0/rels/rel_transpose_3.cvc
new file mode 100644
index 000000000..5dfe3b031
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_3.cvc
@@ -0,0 +1,15 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+ASSERT (x = y);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc b/test/regress/regress0/rels/rel_transpose_4.cvc
new file mode 100644
index 000000000..b260147c8
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_4.cvc
@@ -0,0 +1,13 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+
+ASSERT z IS_IN x;
+ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_5.cvc b/test/regress/regress0/rels/rel_transpose_5.cvc
new file mode 100644
index 000000000..203e8b3d2
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_5.cvc
@@ -0,0 +1,22 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+ASSERT zt IS_IN y;
+
+w : IntPair;
+ASSERT w = (2, 2);
+ASSERT w IS_IN y;
+ASSERT z IS_IN x;
+
+ASSERT NOT (zt IS_IN (TRANSPOSE (x JOIN y)));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_6.cvc b/test/regress/regress0/rels/rel_transpose_6.cvc
new file mode 100644
index 000000000..a2e8bcf10
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_6.cvc
@@ -0,0 +1,24 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+
+ASSERT z IS_IN x;
+ASSERT (3, 4) IS_IN x;
+ASSERT (3, 5) IS_IN x;
+ASSERT (3, 3) IS_IN x;
+
+ASSERT x = TRANSPOSE(y);
+
+ASSERT NOT (zt IS_IN y);
+
+ASSERT z IS_IN y;
+ASSERT NOT (zt IS_IN (TRANSPOSE y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_7.cvc b/test/regress/regress0/rels/rel_transpose_7.cvc
new file mode 100644
index 000000000..bcc3babc8
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_7.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+ASSERT x = y;
+ASSERT NOT (TRANSPOSE(x) =  TRANSPOSE(y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/set-strat.cvc b/test/regress/regress0/rels/set-strat.cvc
new file mode 100644
index 000000000..0dee0e84d
--- /dev/null
+++ b/test/regress/regress0/rels/set-strat.cvc
@@ -0,0 +1,24 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [ INT, INT];
+SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ];
+x : SET OF IntPair;
+y : SET OF IntPair;
+w : SET OF IntPair;
+z : SET OF SetIntPair;
+
+a : IntPair;
+b : IntPair;
+
+ASSERT NOT a = b;
+
+ASSERT a IS_IN x;
+ASSERT b IS_IN y;
+ASSERT b IS_IN w;
+ASSERT (x,y) IS_IN z;
+ASSERT (w,x) IS_IN z;
+ASSERT NOT ( (x,x) IS_IN (z JOIN z) );
+
+ASSERT (x, { ( 0, 0 ) } ) IS_IN (z JOIN z);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/strat.cvc b/test/regress/regress0/rels/strat.cvc
new file mode 100644
index 000000000..b91ddbbe8
--- /dev/null
+++ b/test/regress/regress0/rels/strat.cvc
@@ -0,0 +1,24 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [ INT, INT];
+IntIntPair: TYPE = [ IntPair, IntPair];
+x : SET OF IntIntPair;
+y : SET OF IntIntPair;
+z : SET OF IntPair;
+w : SET OF IntPair;
+
+a : IntPair;
+b : IntPair;
+c : IntIntPair;
+
+ASSERT NOT a = b;
+
+ASSERT a IS_IN z;
+ASSERT b IS_IN z;
+ASSERT (a,b) IS_IN x;
+ASSERT (b,a) IS_IN x;
+ASSERT c IS_IN x;
+ASSERT NOT ( c = (a,b) ) AND NOT ( c = (b,a) );
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/strat_0_1.cvc b/test/regress/regress0/rels/strat_0_1.cvc
new file mode 100644
index 000000000..b91ddbbe8
--- /dev/null
+++ b/test/regress/regress0/rels/strat_0_1.cvc
@@ -0,0 +1,24 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [ INT, INT];
+IntIntPair: TYPE = [ IntPair, IntPair];
+x : SET OF IntIntPair;
+y : SET OF IntIntPair;
+z : SET OF IntPair;
+w : SET OF IntPair;
+
+a : IntPair;
+b : IntPair;
+c : IntIntPair;
+
+ASSERT NOT a = b;
+
+ASSERT a IS_IN z;
+ASSERT b IS_IN z;
+ASSERT (a,b) IS_IN x;
+ASSERT (b,a) IS_IN x;
+ASSERT c IS_IN x;
+ASSERT NOT ( c = (a,b) ) AND NOT ( c = (b,a) );
+
+
+CHECKSAT;