Refactor regressions (#1581)

38 files changed, 0 insertions, 1636 deletions

diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index c8fb739d0..9cdfa5b7b 100644
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -22,18 +22,10 @@ MAKEFLAGS = -k
 # 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 \
@@ -41,83 +33,53 @@ TESTS =	\
   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 \
   rel_tc_8.cvc \
   atom_univ2.cvc \
   rels-sharing-simp.cvc \
   iden_0.cvc \
-  iden_1_1.cvc \
   iden_1.cvc \
-  joinImg_0_1.cvc \
-  joinImg_0_2.cvc \
   joinImg_0.cvc \
-  joinImg_1_1.cvc \
-  joinImg_1.cvc \
-  joinImg_2_1.cvc \
-  joinImg_2.cvc \
   card_transpose.cvc \
   relations-ops.smt2
 
-# unsolved : garbage_collect.cvc
-
 EXTRA_DIST = $(TESTS)
 
 # synonyms for "check"
diff --git a/test/regress/regress0/rels/addr_book_1.cvc b/test/regress/regress0/rels/addr_book_1.cvc
deleted file mode 100644
index 34176f274..000000000
--- a/test/regress/regress0/rels/addr_book_1.cvc
+++ /dev/null
@@ -1,45 +0,0 @@
-% 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
deleted file mode 100644
index 3273ade3a..000000000
--- a/test/regress/regress0/rels/addr_book_1_1.cvc
+++ /dev/null
@@ -1,45 +0,0 @@
-% 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
deleted file mode 100644
index 970ebdc8c..000000000
--- a/test/regress/regress0/rels/bv1-unit.cvc
+++ /dev/null
@@ -1,21 +0,0 @@
-% 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
deleted file mode 100644
index 50a5bb48a..000000000
--- a/test/regress/regress0/rels/bv1-unitb.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% 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
deleted file mode 100644
index 95e7419ba..000000000
--- a/test/regress/regress0/rels/bv1.cvc
+++ /dev/null
@@ -1,20 +0,0 @@
-% 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
deleted file mode 100644
index 5eceb214c..000000000
--- a/test/regress/regress0/rels/bv1p-sat.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% 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
deleted file mode 100644
index 130ccae97..000000000
--- a/test/regress/regress0/rels/bv1p.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% 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
deleted file mode 100644
index d7162de7c..000000000
--- a/test/regress/regress0/rels/bv2.cvc
+++ /dev/null
@@ -1,20 +0,0 @@
-% 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
deleted file mode 100644
index 1fc1f2fea..000000000
--- a/test/regress/regress0/rels/garbage_collect.cvc
+++ /dev/null
@@ -1,60 +0,0 @@
-% 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/iden_1_1.cvc b/test/regress/regress0/rels/iden_1_1.cvc
deleted file mode 100644
index 985a35a89..000000000
--- a/test/regress/regress0/rels/iden_1_1.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% EXPECT: sat
-OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
-Atom:TYPE;
-AtomPair: TYPE = [Atom, Atom];
-x : SET OF AtomPair;
-t : SET OF [Atom];
-univ : SET OF [Atom];
-univ2 : SET OF [Atom,Atom];
-
-a : Atom;
-b : Atom;
-c : Atom;
-d : Atom;
-ASSERT univ = UNIVERSE::SET OF [Atom];
-ASSERT univ2 = UNIVERSE::SET OF [Atom, Atom];
-ASSERT univ2 = (univ PRODUCT univ);
-ASSERT (a, b) IS_IN x;
-ASSERT (c, d) IS_IN x;
-ASSERT NOT(a = b);
-ASSERT IDEN(univ) <= x;
-CHECKSAT;
diff --git a/test/regress/regress0/rels/join-eq-structure-and.cvc b/test/regress/regress0/rels/join-eq-structure-and.cvc
deleted file mode 100644
index 177410b1e..000000000
--- a/test/regress/regress0/rels/join-eq-structure-and.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% 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
deleted file mode 100644
index e27d3811c..000000000
--- a/test/regress/regress0/rels/join-eq-structure.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% 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
deleted file mode 100644
index e27d3811c..000000000
--- a/test/regress/regress0/rels/join-eq-structure_0_1.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% 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/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc
deleted file mode 100644
index 4e69394bd..000000000
--- a/test/regress/regress0/rels/joinImg_0_1.cvc
+++ /dev/null
@@ -1,36 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-OPTION "sets-ext";
-IntPair: TYPE = [INT, INT];
-x : SET OF IntPair;
-y : SET OF IntPair;
-r : SET OF IntPair;
-
-t : SET OF [INT];
-u : SET OF [INT];
-
-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: INT;
-
-ASSERT (1, 7) IS_IN x;
-ASSERT z IS_IN x;
-
-ASSERT (7, 5) IS_IN y;
-
-ASSERT t = (x JOIN_IMAGE 2);
-
-ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2);
-
-ASSERT u = (x JOIN_IMAGE 1);
-
-ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
-
-ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1);
-CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_0_2.cvc b/test/regress/regress0/rels/joinImg_0_2.cvc
deleted file mode 100644
index e15920804..000000000
--- a/test/regress/regress0/rels/joinImg_0_2.cvc
+++ /dev/null
@@ -1,39 +0,0 @@
-% EXPECT: sat
-OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
-IntPair: TYPE = [INT, INT];
-x : SET OF IntPair;
-y : SET OF IntPair;
-r : SET OF IntPair;
-
-t : SET OF [INT];
-u : SET OF [INT];
-univ : SET OF [INT];
-
-z : IntPair;
-ASSERT z = (1,2);
-zt : IntPair;
-ASSERT zt = (2,1);
-s : IntPair;
-ASSERT s = (1,1);
-a : IntPair;
-ASSERT a = (1,5);
-b: INT;
-
-ASSERT (1, 7) IS_IN x;
-ASSERT z IS_IN x;
-
-ASSERT (7, 5) IS_IN y;
-
-ASSERT t = (x JOIN_IMAGE 2);
-ASSERT univ = (x JOIN_IMAGE 0);
-ASSERT TUPLE(100) IS_IN t;
-
-ASSERT NOT (TUPLE(3) IS_IN univ);
-
-ASSERT u = (x JOIN_IMAGE 1);
-
-ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
-
-ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1);
-CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc
deleted file mode 100644
index 81f208fc4..000000000
--- a/test/regress/regress0/rels/joinImg_1.cvc
+++ /dev/null
@@ -1,21 +0,0 @@
-% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
-OPTION "sets-ext";
-Atom: TYPE;
-x : SET OF [Atom, Atom];
-y : SET OF [Atom, Atom];
-r : SET OF [Atom, Atom];
-
-t : SET OF [Atom];
-
-a : Atom;
-b : Atom;
-c : Atom;
-d : Atom;
-e : Atom;
-
-ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
-ASSERT x = {(b, c), (d, e), (c, e)};
-ASSERT NOT(a = b);
-
-CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc
deleted file mode 100644
index 003770a1b..000000000
--- a/test/regress/regress0/rels/joinImg_1_1.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-OPTION "sets-ext";
-Atom: TYPE;
-x : SET OF [Atom, Atom];
-y : SET OF [Atom, Atom];
-r : SET OF [Atom, Atom];
-
-t : SET OF [Atom];
-
-a : Atom;
-b : Atom;
-c : Atom;
-d : Atom;
-e : Atom;
-
-ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
-ASSERT t = (x JOIN_IMAGE 2); 
-ASSERT x = {(b, c), (d, e), (c, e)};
-ASSERT TUPLE(c) IS_IN t;
-
-CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc
deleted file mode 100644
index a4acfe6c6..000000000
--- a/test/regress/regress0/rels/joinImg_2.cvc
+++ /dev/null
@@ -1,34 +0,0 @@
-% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
-OPTION "sets-ext";
-Atom: TYPE;
-x : SET OF [Atom, Atom];
-y : SET OF [Atom, Atom];
-r : SET OF [Atom, Atom];
-
-t : SET OF [Atom];
-
-a : Atom;
-b : Atom;
-c : Atom;
-d : Atom;
-e : Atom;
-f : Atom;
-g : Atom;
-
-ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
-ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3);
-%ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
-ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)};
-ASSERT (a, f) IS_IN x;
-ASSERT (a, f) IS_IN y;
-ASSERT x = y;
-
-
-
-ASSERT NOT(a = b);
-
-ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2));
-ASSERT f = d;
-
-CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc
deleted file mode 100644
index 03f88be37..000000000
--- a/test/regress/regress0/rels/joinImg_2_1.cvc
+++ /dev/null
@@ -1,25 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-OPTION "sets-ext";
-Atom: TYPE;
-x : SET OF [Atom, Atom];
-y : SET OF [Atom, Atom];
-r : SET OF [Atom, Atom];
-
-t : SET OF [Atom];
-
-a : Atom;
-b : Atom;
-c : Atom;
-d : Atom;
-e : Atom;
-f : Atom;
-g : Atom;
-
-ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
-ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1);
-ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
-ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
-ASSERT (NOT(a = b)) OR (NOT(a = f));
-
-CHECKSAT;
diff --git a/test/regress/regress0/rels/prod-mod-eq.cvc b/test/regress/regress0/rels/prod-mod-eq.cvc
deleted file mode 100644
index 96ef2ffba..000000000
--- a/test/regress/regress0/rels/prod-mod-eq.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% 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
deleted file mode 100644
index b9341a216..000000000
--- a/test/regress/regress0/rels/prod-mod-eq2.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% 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_complex_3.cvc b/test/regress/regress0/rels/rel_complex_3.cvc
deleted file mode 100644
index 492c94432..000000000
--- a/test/regress/regress0/rels/rel_complex_3.cvc
+++ /dev/null
@@ -1,49 +0,0 @@
-% 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
deleted file mode 100644
index f473b00aa..000000000
--- a/test/regress/regress0/rels/rel_complex_4.cvc
+++ /dev/null
@@ -1,52 +0,0 @@
-% 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
deleted file mode 100644
index d64817187..000000000
--- a/test/regress/regress0/rels/rel_complex_5.cvc
+++ /dev/null
@@ -1,55 +0,0 @@
-% 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_mix_0_1.cvc b/test/regress/regress0/rels/rel_mix_0_1.cvc
deleted file mode 100644
index 723a9b2e2..000000000
--- a/test/regress/regress0/rels/rel_mix_0_1.cvc
+++ /dev/null
@@ -1,30 +0,0 @@
-% 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
deleted file mode 100644
index 6cdf03600..000000000
--- a/test/regress/regress0/rels/rel_pressure_0.cvc
+++ /dev/null
@@ -1,617 +0,0 @@
-% 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_tc_10_1.cvc b/test/regress/regress0/rels/rel_tc_10_1.cvc
deleted file mode 100644
index 67c444070..000000000
--- a/test/regress/regress0/rels/rel_tc_10_1.cvc
+++ /dev/null
@@ -1,18 +0,0 @@
-% 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_4.cvc b/test/regress/regress0/rels/rel_tc_4.cvc
deleted file mode 100644
index decd38fe1..000000000
--- a/test/regress/regress0/rels/rel_tc_4.cvc
+++ /dev/null
@@ -1,19 +0,0 @@
-% 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
deleted file mode 100644
index 8ee75f7e9..000000000
--- a/test/regress/regress0/rels/rel_tc_4_1.cvc
+++ /dev/null
@@ -1,10 +0,0 @@
-% 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
deleted file mode 100644
index fd9caeade..000000000
--- a/test/regress/regress0/rels/rel_tc_5_1.cvc
+++ /dev/null
@@ -1,9 +0,0 @@
-% 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
deleted file mode 100644
index 4570c5a8d..000000000
--- a/test/regress/regress0/rels/rel_tc_6.cvc
+++ /dev/null
@@ -1,9 +0,0 @@
-% 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_9_1.cvc b/test/regress/regress0/rels/rel_tc_9_1.cvc
deleted file mode 100644
index f884349b1..000000000
--- a/test/regress/regress0/rels/rel_tc_9_1.cvc
+++ /dev/null
@@ -1,23 +0,0 @@
-% 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
deleted file mode 100644
index 441e79c45..000000000
--- a/test/regress/regress0/rels/rel_tp_2.cvc
+++ /dev/null
@@ -1,10 +0,0 @@
-% 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_join_2_1.cvc b/test/regress/regress0/rels/rel_tp_join_2_1.cvc
deleted file mode 100644
index acf3dbccf..000000000
--- a/test/regress/regress0/rels/rel_tp_join_2_1.cvc
+++ /dev/null
@@ -1,19 +0,0 @@
-% 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/set-strat.cvc b/test/regress/regress0/rels/set-strat.cvc
deleted file mode 100644
index 0dee0e84d..000000000
--- a/test/regress/regress0/rels/set-strat.cvc
+++ /dev/null
@@ -1,24 +0,0 @@
-% 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
deleted file mode 100644
index b91ddbbe8..000000000
--- a/test/regress/regress0/rels/strat.cvc
+++ /dev/null
@@ -1,24 +0,0 @@
-% 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
deleted file mode 100644
index b91ddbbe8..000000000
--- a/test/regress/regress0/rels/strat_0_1.cvc
+++ /dev/null
@@ -1,24 +0,0 @@
-% 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;