From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 29 Sep 2021 18:40:08 +0000 (-0500)
Subject: Update the syntax for tuples in smt2 (#7265)
X-Git-Tag: cvc5-1.0.0~1159
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e86726da4cf3883888a765aacf81ae76c7611c54;p=cvc5.git

Update the syntax for tuples in smt2 (#7265)

This changes mkTuple -> tuple and tupSel -> tuple_select.

This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.
---

diff --git a/examples/api/smtlib/relations.smt2 b/examples/api/smtlib/relations.smt2
index 11801a868..b663b7f17 100644
--- a/examples/api/smtlib/relations.smt2
+++ b/examples/api/smtlib/relations.smt2
@@ -13,17 +13,17 @@
 (assert
   (= r1
     (insert
-      (mkTuple "a" 1)
-      (mkTuple "b" 2)
-      (mkTuple "c" 3)
-      (singleton (mkTuple "d" 4)))))
+      (tuple "a" 1)
+      (tuple "b" 2)
+      (tuple "c" 3)
+      (singleton (tuple "d" 4)))))
 (assert
   (= r2
     (insert
-      (mkTuple 1 "1")
-      (mkTuple 2 "2")
-      (mkTuple 3 "3")
-      (singleton (mkTuple 17 "17")))))
+      (tuple 1 "1")
+      (tuple 2 "2")
+      (tuple 3 "3")
+      (singleton (tuple 17 "17")))))
 (assert (= r (join r1 r2)))
 (assert (= s (transpose r)))
 (assert (= t (product r1 r2)))
@@ -31,10 +31,10 @@
   (=
     lt1
      (insert
-       (mkTuple 1 2)
-       (mkTuple 2 3)
-       (mkTuple 3 4)
-       (singleton (mkTuple 4 5)))))
+       (tuple 1 2)
+       (tuple 2 3)
+       (tuple 3 4)
+       (singleton (tuple 4 5)))))
 (assert (= lt2 (tclosure lt1)))
 (assert (= i (card t)))
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 674aeca1f..623b0aedd 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2332,8 +2332,8 @@ FORALL_TOK        : 'forall';
 
 EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
-TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
-TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
+TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple';
+TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select';
 TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
 
 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f9bca8535..cf3f68308 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -736,7 +736,7 @@ void Smt2Printer::toStream(std::ostream& out,
     if (dt.isTuple())
     {
       stillNeedToPrintParams = false;
-      out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
+      out << "tuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
     }
     break;
   }
@@ -768,7 +768,7 @@ void Smt2Printer::toStream(std::ostream& out,
     if (dt.isTuple())
     {
       stillNeedToPrintParams = false;
-      out << "(_ tupSel " << DType::indexOf(op) << ") ";
+      out << "(_ tuple_select " << DType::indexOf(op) << ") ";
     }
   }
   break;
diff --git a/test/regress/regress0/bug596b.cvc.smt2 b/test/regress/regress0/bug596b.cvc.smt2
index 120966bf0..3482f6a37 100644
--- a/test/regress/regress0/bug596b.cvc.smt2
+++ b/test/regress/regress0/bug596b.cvc.smt2
@@ -3,5 +3,5 @@
 (set-option :incremental false)
 (declare-fun f (Int) (Tuple Int Bool))
 (declare-fun a () Int)
-(assert (not (= (f a) (mkTuple 0 false))))
+(assert (not (= (f a) (tuple 0 false))))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/4482-unc-simp-one.smt2 b/test/regress/regress0/datatypes/4482-unc-simp-one.smt2
index 265aeef23..a48b68535 100644
--- a/test/regress/regress0/datatypes/4482-unc-simp-one.smt2
+++ b/test/regress/regress0/datatypes/4482-unc-simp-one.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun a () Tuple)
-(assert (distinct a mkTuple))
+(assert (distinct a tuple))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2 b/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2
index 87847d635..f4ac5f7e5 100644
--- a/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2
+++ b/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2
@@ -3,6 +3,6 @@
 (set-option :incremental false)
 
 (declare-fun test (Int) (Tuple Int Int))
-(assert (= (test 5) (mkTuple 2 3)))
-(assert (= (test 7) (mkTuple 3 4)))
+(assert (= (test 5) (tuple 2 3)))
+(assert (= (test 7) (tuple 3 4)))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2 b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2
index 7f391b719..7f666db79 100644
--- a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2
+++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2
@@ -2,5 +2,5 @@
 (set-logic ALL)
 (set-option :incremental false)
 (declare-fun x () (Tuple Int Bool))
-(assert (not (= x (mkTuple 0 false))))
+(assert (not (= x (tuple 0 false))))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2 b/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2
index d581b37b9..e05a65ad0 100644
--- a/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2
+++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2
@@ -4,7 +4,7 @@
 (declare-datatypes ((list 1)) ((par (T)((cons (car T) (care Bool) (cdr (list T))) (nil)))))
 (declare-fun x () (list Real))
 (declare-fun y () (Tuple Int Bool Int))
-(assert (= y (mkTuple 5 true 4)))
-(assert ((_ tupSel 1) y))
+(assert (= y (tuple 5 true 4)))
+(assert ((_ tuple_select 1) y))
 (assert (= x ((as cons (list Real)) (/ 11 10) true (as nil (list Real)))))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/tuple-model.cvc.smt2 b/test/regress/regress0/datatypes/tuple-model.cvc.smt2
index dcd68d03a..7f063a499 100644
--- a/test/regress/regress0/datatypes/tuple-model.cvc.smt2
+++ b/test/regress/regress0/datatypes/tuple-model.cvc.smt2
@@ -2,5 +2,5 @@
 (set-logic ALL)
 (set-option :incremental false)
 (declare-fun x () (Tuple Int Int))
-(assert (= ((_ tupSel 0) x) 5))
+(assert (= ((_ tuple_select 0) x) 5))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2 b/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2
index 1d05489b3..0c9479f07 100644
--- a/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2
+++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2
@@ -4,6 +4,6 @@
 (declare-fun x () (Tuple Real Real))
 (declare-fun y () Real)
 (declare-fun z () Real)
-(assert (or (= x (mkTuple y z)) (= x (mkTuple z y))))
-(assert (let ((_let_1 1.0)) (let ((_let_2 0.0)) (or (= x (mkTuple _let_2 _let_2)) (= x (mkTuple _let_1 _let_1))))))
+(assert (or (= x (tuple y z)) (= x (tuple z y))))
+(assert (let ((_let_1 1.0)) (let ((_let_2 0.0)) (or (= x (tuple _let_2 _let_2)) (= x (tuple _let_1 _let_1))))))
 (check-sat)
diff --git a/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2 b/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2
index 433a79797..f26769ccc 100644
--- a/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2
+++ b/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2
@@ -7,5 +7,5 @@
 (declare-fun x () Int)
 (define-fun foo ((x |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)) |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| ((_ update int) x (int x)))
 (declare-fun m () |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)
-(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (mkTuple (foo m) 0) (mkTuple m 0)))
-(check-sat-assuming ( (not (= ((_ tupSel 1) (ite (= x 0) (mkTuple (foo m) 0) (mkTuple m 0))) 1)) ))
+(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (tuple (foo m) 0) (tuple m 0)))
+(check-sat-assuming ( (not (= ((_ tuple_select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) ))
diff --git a/test/regress/regress0/datatypes/tuple.cvc.smt2 b/test/regress/regress0/datatypes/tuple.cvc.smt2
index 2b0959968..9e6e83c2b 100644
--- a/test/regress/regress0/datatypes/tuple.cvc.smt2
+++ b/test/regress/regress0/datatypes/tuple.cvc.smt2
@@ -1,10 +1,10 @@
 ; EXPECT: unsat
 (set-logic ALL)
 (set-option :incremental false)
-(define-fun x () (Tuple Real Int Real) (mkTuple (/ 4 5) 9 (/ 11 9)))
-(define-fun first_elem () Real ((_ tupSel 0) (mkTuple (/ 4 5) 9 (/ 11 9))))
-(define-fun third_elem () Real ((_ tupSel 2) (mkTuple (/ 4 5) 9 (/ 11 9))))
+(define-fun x () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))
+(define-fun first_elem () Real ((_ tuple_select 0) (tuple (/ 4 5) 9 (/ 11 9))))
+(define-fun third_elem () Real ((_ tuple_select 2) (tuple (/ 4 5) 9 (/ 11 9))))
 
-(define-fun y () (Tuple Real Int Real) (mkTuple (/ 4 5) 9 (/ 11 9)))
-(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (mkTuple (/ 4 5) 9 (/ 11 9)) 3))
-(check-sat-assuming ( (not (let ((_let_1 (mkTuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tupSel 0) _let_1) ((_ tupSel 0) _let_2))) (= ((_ tupSel 2) _let_1) ((_ tupSel 2) _let_2))) (= ((_ tupSel 1) _let_2) 3))))) ))
+(define-fun y () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))
+(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3))
+(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple_select 0) _let_1) ((_ tuple_select 0) _let_2))) (= ((_ tuple_select 2) _let_1) ((_ tuple_select 2) _let_2))) (= ((_ tuple_select 1) _let_2) 3))))) ))
diff --git a/test/regress/regress0/datatypes/tuples-empty.smt2 b/test/regress/regress0/datatypes/tuples-empty.smt2
index ec7e36ca8..125548499 100644
--- a/test/regress/regress0/datatypes/tuples-empty.smt2
+++ b/test/regress/regress0/datatypes/tuples-empty.smt2
@@ -7,8 +7,8 @@
 (declare-fun t1 () (Tuple (Tuple Int Int) (Tuple Int String Int)))
 (declare-fun t2 () (Tuple (Tuple Bool Int) String))
 
-(assert (= t1 (mkTuple (mkTuple 12 99) (mkTuple 5 "xyz" 17))))
-(assert (= t2 (mkTuple (mkTuple true 14) "abc")))
-(assert (= t mkTuple))
+(assert (= t1 (tuple (tuple 12 99) (tuple 5 "xyz" 17))))
+(assert (= t2 (tuple (tuple true 14) "abc")))
+(assert (= t tuple))
 
 (check-sat)
diff --git a/test/regress/regress0/datatypes/tuples-multitype.smt2 b/test/regress/regress0/datatypes/tuples-multitype.smt2
index 8e412f2ed..c6555c5df 100644
--- a/test/regress/regress0/datatypes/tuples-multitype.smt2
+++ b/test/regress/regress0/datatypes/tuples-multitype.smt2
@@ -5,7 +5,7 @@
 (declare-fun t () (Tuple Int String))
 (declare-fun i () String)
 
-(assert (= t (mkTuple 0 "0")))
-(assert (= i ((_ tupSel 1) t)))
+(assert (= t (tuple 0 "0")))
+(assert (= i ((_ tuple_select 1) t)))
 
 (check-sat)
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 b/test/regress/regress0/fmf/quant_real_univ.cvc.smt2
index f4724355b..68fee3f21 100644
--- a/test/regress/regress0/fmf/quant_real_univ.cvc.smt2
+++ b/test/regress/regress0/fmf/quant_real_univ.cvc.smt2
@@ -9,5 +9,5 @@
 (assert (= REAL_UNIVERSE (as univset (Set (Tuple Real)))))
 (assert (= ATOM_UNIVERSE (as univset (Set (Tuple Atom)))))
 (declare-fun levelVal () (Set (Tuple Atom Real)))
-(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (member (mkTuple s) ATOM_UNIVERSE) (member (mkTuple v1) REAL_UNIVERSE)) (member (mkTuple v2) REAL_UNIVERSE)) (=> (and (member (mkTuple s v1) levelVal) (member (mkTuple s v2) levelVal)) (= v1 v2)))))
+(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (member (tuple s) ATOM_UNIVERSE) (member (tuple v1) REAL_UNIVERSE)) (member (tuple v2) REAL_UNIVERSE)) (=> (and (member (tuple s v1) levelVal) (member (tuple s v2) levelVal)) (= v1 v2)))))
 (check-sat)
diff --git a/test/regress/regress0/printer/tuples_and_records.cvc.smt2 b/test/regress/regress0/printer/tuples_and_records.cvc.smt2
index 49d12d1c0..0c54f5f49 100644
--- a/test/regress/regress0/printer/tuples_and_records.cvc.smt2
+++ b/test/regress/regress0/printer/tuples_and_records.cvc.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
 ; EXPECT: (((a r) "active"))
-; EXPECT: ((((_ tupSel 1) y) 9))
+; EXPECT: ((((_ tuple_select 1) y) 9))
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :produce-models true)
@@ -9,7 +9,7 @@
 (declare-fun r () __cvc5_record_a_String_b_String)
 (declare-fun y () (Tuple Real Int Real))
 (assert (= r (__cvc5_record_a_String_b_String_ctor "active" "who knows?")))
-(assert (= y (mkTuple (/ 4 5) 9 (/ 11 9))))
+(assert (= y (tuple (/ 4 5) 9 (/ 11 9))))
 (check-sat-assuming ( (not (= (a r) "what?")) ))
 (get-value ( (a r) ))
-(get-value ( ((_ tupSel 1) y) ))
+(get-value ( ((_ tuple_select 1) y) ))
diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2
index a27be5b4b..00fc33d56 100644
--- a/test/regress/regress0/rels/addr_book_0.cvc.smt2
+++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2
@@ -13,23 +13,23 @@
 (declare-fun addr () (Set (Tuple Atom Atom Atom)))
 (declare-fun b1 () Atom)
 (declare-fun b1_tup () (Tuple Atom))
-(assert (= b1_tup (mkTuple b1)))
+(assert (= b1_tup (tuple b1)))
 (assert (member b1_tup Book))
 (declare-fun b2 () Atom)
 (declare-fun b2_tup () (Tuple Atom))
-(assert (= b2_tup (mkTuple b2)))
+(assert (= b2_tup (tuple b2)))
 (assert (member b2_tup Book))
 (declare-fun b3 () Atom)
 (declare-fun b3_tup () (Tuple Atom))
-(assert (= b3_tup (mkTuple b3)))
+(assert (= b3_tup (tuple b3)))
 (assert (member b3_tup Book))
 (declare-fun n () Atom)
 (declare-fun n_tup () (Tuple Atom))
-(assert (= n_tup (mkTuple n)))
+(assert (= n_tup (tuple n)))
 (assert (member n_tup Name))
 (declare-fun t () Atom)
 (declare-fun t_tup () (Tuple Atom))
-(assert (= t_tup (mkTuple t)))
+(assert (= t_tup (tuple t)))
 (assert (member t_tup Target))
 (assert (subset (join (join Book addr) Target) Name))
 (assert (subset (join Book names) Name))
diff --git a/test/regress/regress0/rels/atom_univ2.cvc.smt2 b/test/regress/regress0/rels/atom_univ2.cvc.smt2
index 0fba2f00c..ad7d5ec4b 100644
--- a/test/regress/regress0/rels/atom_univ2.cvc.smt2
+++ b/test/regress/regress0/rels/atom_univ2.cvc.smt2
@@ -8,10 +8,10 @@
 (declare-fun x () Atom)
 (declare-fun y () Atom)
 (assert (not (= x y)))
-(assert (member (mkTuple y) a))
-(assert (member (mkTuple x y) b))
+(assert (member (tuple y) a))
+(assert (member (tuple x y) b))
 (assert (= (as univset (Set (Tuple Atom Atom))) (product (as univset (Set (Tuple Atom))) (as univset (Set (Tuple Atom))))))
 (declare-fun u () (Set (Tuple Atom Atom)))
 (assert (= u (as univset (Set (Tuple Atom Atom)))))
-(assert (not (member (mkTuple x y) u)))
+(assert (not (member (tuple x y) u)))
 (check-sat)
diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2
index fca943912..d2d091e60 100644
--- a/test/regress/regress0/rels/iden_0.cvc.smt2
+++ b/test/regress/regress0/rels/iden_0.cvc.smt2
@@ -7,19 +7,19 @@
 (declare-fun id () (Set (Tuple Int Int)))
 (declare-fun t () (Set (Tuple Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1) t))
-(assert (member (mkTuple 2) t))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1) t))
+(assert (member (tuple 2) t))
 (assert (member z x))
 (assert (member zt x))
 (assert (member v x))
 (assert (member a x))
 (assert (= id (iden t)))
-(assert (not (member (mkTuple 1 1) (intersection id x))))
+(assert (not (member (tuple 1 1) (intersection id x))))
 (check-sat)
diff --git a/test/regress/regress0/rels/iden_1.cvc.smt2 b/test/regress/regress0/rels/iden_1.cvc.smt2
index 5a59eda53..c2de24558 100644
--- a/test/regress/regress0/rels/iden_1.cvc.smt2
+++ b/test/regress/regress0/rels/iden_1.cvc.smt2
@@ -12,8 +12,8 @@
 (declare-fun c () Atom)
 (declare-fun d () Atom)
 (assert (= univ (as univset (Set (Tuple Atom)))))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple c d) x))
+(assert (member (tuple a b) x))
+(assert (member (tuple c d) x))
 (assert (not (= a b)))
 (assert (= (iden (join x univ)) x))
 (check-sat)
diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 b/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2
index 3801be252..37af1b418 100644
--- a/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2
+++ b/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2
@@ -10,9 +10,9 @@
 (declare-fun w () (Set (Tuple Int unit)))
 (declare-fun z () (Set (Tuple unit Int)))
 (assert (= (join x y) (join w z)))
-(assert (member (mkTuple 0 1) (join x y)))
-(assert (member (mkTuple 0 u) w))
+(assert (member (tuple 0 1) (join x y)))
+(assert (member (tuple 0 u) w))
 (declare-fun t () Int)
 (assert (and (> t 0) (< t 3)))
-(assert (not (member (mkTuple u t) z)))
+(assert (not (member (tuple u t) z)))
 (check-sat)
diff --git a/test/regress/regress0/rels/join-eq-u.cvc.smt2 b/test/regress/regress0/rels/join-eq-u.cvc.smt2
index a455e1d36..92514a3be 100644
--- a/test/regress/regress0/rels/join-eq-u.cvc.smt2
+++ b/test/regress/regress0/rels/join-eq-u.cvc.smt2
@@ -10,9 +10,9 @@
 (declare-fun w () (Set (Tuple Int unit)))
 (declare-fun z () (Set (Tuple unit Int)))
 (assert (= (join x y) (join w z)))
-(assert (member (mkTuple 0 1) (join x y)))
-(assert (member (mkTuple 0 u) w))
+(assert (member (tuple 0 1) (join x y)))
+(assert (member (tuple 0 u) w))
 (declare-fun t () Int)
 (assert (and (> t 0) (< t 2)))
-(assert (not (member (mkTuple u t) z)))
+(assert (not (member (tuple u t) z)))
 (check-sat)
diff --git a/test/regress/regress0/rels/joinImg_0.cvc.smt2 b/test/regress/regress0/rels/joinImg_0.cvc.smt2
index a2ae87de9..76a13b645 100644
--- a/test/regress/regress0/rels/joinImg_0.cvc.smt2
+++ b/test/regress/regress0/rels/joinImg_0.cvc.smt2
@@ -8,19 +8,19 @@
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun t () (Set (Tuple Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
 (assert (member z x))
-(assert (member (mkTuple 7 5) y))
+(assert (member (tuple 7 5) y))
 (assert (= t (join_image x 2)))
-(assert (member (mkTuple 3) (join_image x 2)))
-(assert (not (member (mkTuple 1) (join_image x 2))))
-(assert (member (mkTuple 4) (join_image x 2)))
-(assert (member (mkTuple 1) (join_image x 1)))
+(assert (member (tuple 3) (join_image x 2)))
+(assert (not (member (tuple 1) (join_image x 2))))
+(assert (member (tuple 4) (join_image x 2)))
+(assert (member (tuple 1) (join_image x 1)))
 (check-sat)
diff --git a/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2 b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
index 4beb03a76..c04aa7985 100644
--- a/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
+++ b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
@@ -8,6 +8,6 @@
 (declare-fun c () Atom)
 (declare-fun J ((Set (Tuple Atom)) (Set (Tuple Atom Atom))) (Set (Tuple Atom)))
 (declare-fun T ((Set (Tuple Atom Atom))) (Set (Tuple Atom Atom)))
-(assert (let ((_let_1 (singleton (mkTuple a)))) (= (join _let_1 t) (J _let_1 t))))
-(assert (let ((_let_1 (singleton (mkTuple c)))) (not (= (join _let_1 (tclosure t)) _let_1))))
+(assert (let ((_let_1 (singleton (tuple a)))) (= (join _let_1 t) (J _let_1 t))))
+(assert (let ((_let_1 (singleton (tuple c)))) (not (= (join _let_1 (tclosure t)) _let_1))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 b/test/regress/regress0/rels/rel_1tup_0.cvc.smt2
index 0d0ccbfdc..4210a5486 100644
--- a/test/regress/regress0/rels/rel_1tup_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_1tup_0.cvc.smt2
@@ -7,13 +7,13 @@
 (declare-fun y () (Set (Tuple Int)))
 (declare-fun z () (Set (Tuple Int)))
 (declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 2 1)))
+(assert (= b (tuple 2 1)))
 (assert (member b x))
 (declare-fun a () (Tuple Int))
-(assert (= a (mkTuple 1)))
+(assert (= a (tuple 1)))
 (assert (member a y))
 (declare-fun c () (Tuple Int))
-(assert (= c (mkTuple 2)))
+(assert (= c (tuple 2)))
 (assert (= z (join x y)))
 (assert (not (member c z)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_complex_0.cvc.smt2 b/test/regress/regress0/rels/rel_complex_0.cvc.smt2
index f7705987d..2f4aea539 100644
--- a/test/regress/regress0/rels/rel_complex_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_complex_0.cvc.smt2
@@ -9,15 +9,15 @@
 (declare-fun f () Int)
 (declare-fun g () Int)
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 f)))
+(assert (= e (tuple 4 f)))
 (assert (member e x))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple g 3)))
+(assert (= d (tuple g 3)))
 (assert (member d y))
 (assert (= z (union (singleton f) (singleton g))))
 (assert (= 0 (- f g)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 3)))
+(assert (= a (tuple 4 3)))
 (assert (= r (join x y)))
 (assert (not (member a r)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_complex_1.cvc.smt2 b/test/regress/regress0/rels/rel_complex_1.cvc.smt2
index 823fb7ed1..e8ccfb070 100644
--- a/test/regress/regress0/rels/rel_complex_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_complex_1.cvc.smt2
@@ -10,18 +10,18 @@
 (declare-fun z () (Set (Tuple Int)))
 (declare-fun r2 () (Set (Tuple Int Int)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 3 1)))
+(assert (= a (tuple 3 1)))
 (assert (member a x))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 1 3)))
+(assert (= d (tuple 1 3)))
 (assert (member d y))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
 (assert (= r (join x y)))
-(assert (member (mkTuple 1) w))
-(assert (member (mkTuple 2) z))
+(assert (member (tuple 1) w))
+(assert (member (tuple 2) z))
 (assert (= r2 (product w z)))
 (assert (not (member e r)))
 (assert (subset r r2))
-(assert (not (member (mkTuple 3 3) r2)))
+(assert (not (member (tuple 3 3) r2)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 b/test/regress/regress0/rels/rel_conflict_0.cvc.smt2
index 4af1f8530..e074778c5 100644
--- a/test/regress/regress0/rels/rel_conflict_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_conflict_0.cvc.smt2
@@ -4,7 +4,7 @@
 
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 4)))
+(assert (= e (tuple 4 4)))
 (assert (member e x))
-(assert (not (member (mkTuple 4 4) x)))
+(assert (not (member (tuple 4 4) x)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_join_0.cvc.smt2 b/test/regress/regress0/rels/rel_join_0.cvc.smt2
index 3e4a68377..3c36d36e8 100644
--- a/test/regress/regress0/rels/rel_join_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_0.cvc.smt2
@@ -6,15 +6,15 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 7 5) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 7 5) y))
 (assert (member z x))
 (assert (member zt y))
 (assert (not (member a (join x y))))
diff --git a/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_0_1.cvc.smt2
index 1c8f7b472..6af8429d3 100644
--- a/test/regress/regress0/rels/rel_join_0_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_0_1.cvc.smt2
@@ -6,16 +6,16 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 4 3) x))
-(assert (member (mkTuple 7 5) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 4 3) x))
+(assert (member (tuple 7 5) y))
 (assert (member z x))
 (assert (member zt y))
 (assert (member a (join x y)))
diff --git a/test/regress/regress0/rels/rel_join_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_1.cvc.smt2
index 22e5e7f8f..88f8c73f3 100644
--- a/test/regress/regress0/rels/rel_join_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_1.cvc.smt2
@@ -6,19 +6,19 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
 (assert (member z x))
 (assert (member zt y))
 (assert (not (member a (join x y))))
diff --git a/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_1_1.cvc.smt2
index 54e51cfe6..e1556149c 100644
--- a/test/regress/regress0/rels/rel_join_1_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_1_1.cvc.smt2
@@ -6,19 +6,19 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
 (assert (member z x))
 (assert (member zt y))
 (assert (= r (join x y)))
diff --git a/test/regress/regress0/rels/rel_join_2.cvc.smt2 b/test/regress/regress0/rels/rel_join_2.cvc.smt2
index 0ab915f7e..5c8f0ea91 100644
--- a/test/regress/regress0/rels/rel_join_2.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_2.cvc.smt2
@@ -6,11 +6,11 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 2 1 3)))
+(assert (= zt (tuple 2 1 3)))
 (declare-fun a () (Tuple Int Int Int))
-(assert (= a (mkTuple 1 1 3)))
+(assert (= a (tuple 1 1 3)))
 (assert (member z x))
 (assert (member zt y))
 (assert (not (member a (join x y))))
diff --git a/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_2_1.cvc.smt2
index 47269ef64..82433cc1b 100644
--- a/test/regress/regress0/rels/rel_join_2_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_2_1.cvc.smt2
@@ -6,11 +6,11 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 2 1 3)))
+(assert (= zt (tuple 2 1 3)))
 (declare-fun a () (Tuple Int Int Int))
-(assert (= a (mkTuple 1 1 3)))
+(assert (= a (tuple 1 1 3)))
 (assert (member z x))
 (assert (member zt y))
 (assert (member a (join x y)))
diff --git a/test/regress/regress0/rels/rel_join_3.cvc.smt2 b/test/regress/regress0/rels/rel_join_3.cvc.smt2
index e726271d1..4a3358526 100644
--- a/test/regress/regress0/rels/rel_join_3.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_3.cvc.smt2
@@ -6,19 +6,19 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
 (assert (= r (join x y)))
 (assert (member z x))
 (assert (member zt y))
diff --git a/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_3_1.cvc.smt2
index 3b06bfb38..7b66ab443 100644
--- a/test/regress/regress0/rels/rel_join_3_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_3_1.cvc.smt2
@@ -6,19 +6,19 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
 (assert (= r (join x y)))
 (assert (member z x))
 (assert (member zt y))
diff --git a/test/regress/regress0/rels/rel_join_4.cvc.smt2 b/test/regress/regress0/rels/rel_join_4.cvc.smt2
index 76ad33633..bc4f16513 100644
--- a/test/regress/regress0/rels/rel_join_4.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_4.cvc.smt2
@@ -6,21 +6,21 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
+(assert (= a (tuple 1 5)))
 (declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 7 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
+(assert (= b (tuple 7 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
 (assert (member b y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
 (assert (= r (join x y)))
 (assert (member z x))
 (assert (member zt y))
diff --git a/test/regress/regress0/rels/rel_join_5.cvc.smt2 b/test/regress/regress0/rels/rel_join_5.cvc.smt2
index 1d138befa..227395fe6 100644
--- a/test/regress/regress0/rels/rel_join_5.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_5.cvc.smt2
@@ -6,13 +6,13 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 4)))
+(assert (= a (tuple 1 4)))
 (assert (= r (join (join (transpose x) y) z)))
 (assert (not (member a r)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_join_6.cvc.smt2 b/test/regress/regress0/rels/rel_join_6.cvc.smt2
index 391bd0fad..547430c19 100644
--- a/test/regress/regress0/rels/rel_join_6.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_6.cvc.smt2
@@ -5,7 +5,7 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
-(assert (= x (union (singleton (mkTuple 1 2)) (singleton (mkTuple 3 4)))))
-(assert (= y (join x (union (singleton (mkTuple 2 1)) (singleton (mkTuple 4 3))))))
-(assert (not (member (mkTuple 1 1) y)))
+(assert (= x (union (singleton (tuple 1 2)) (singleton (tuple 3 4)))))
+(assert (= y (join x (union (singleton (tuple 2 1)) (singleton (tuple 4 3))))))
+(assert (not (member (tuple 1 1) y)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_join_7.cvc.smt2 b/test/regress/regress0/rels/rel_join_7.cvc.smt2
index 6488df50e..3956af748 100644
--- a/test/regress/regress0/rels/rel_join_7.cvc.smt2
+++ b/test/regress/regress0/rels/rel_join_7.cvc.smt2
@@ -7,15 +7,15 @@
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun w () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 7 5) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 7 5) y))
 (assert (member z x))
 (assert (member zt y))
 (assert (= w (union r (join x y))))
diff --git a/test/regress/regress0/rels/rel_product_0.cvc.smt2 b/test/regress/regress0/rels/rel_product_0.cvc.smt2
index 1b9f4e369..890c6f5d6 100644
--- a/test/regress/regress0/rels/rel_product_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_product_0.cvc.smt2
@@ -7,11 +7,11 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int Int Int))
-(assert (= v (mkTuple 1 2 2 1)))
+(assert (= v (tuple 1 2 2 1)))
 (assert (member z x))
 (assert (member zt y))
 (assert (not (member v (product x y))))
diff --git a/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_0_1.cvc.smt2
index 2929a51ee..1958036d2 100644
--- a/test/regress/regress0/rels/rel_product_0_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_product_0_1.cvc.smt2
@@ -7,11 +7,11 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int Int Int))
-(assert (= v (mkTuple 1 2 2 1)))
+(assert (= v (tuple 1 2 2 1)))
 (assert (member z x))
 (assert (member zt y))
 (assert (member v (product x y)))
diff --git a/test/regress/regress0/rels/rel_product_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_1.cvc.smt2
index 93d2eb725..6711cfd6f 100644
--- a/test/regress/regress0/rels/rel_product_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_product_1.cvc.smt2
@@ -7,11 +7,11 @@
 (declare-fun y () (Set (Tuple Int Int Int)))
 (declare-fun r () (Set (Tuple Int Int Int)))
 (declare-fun z () (Tuple Int Int Int))
-(assert (= z (mkTuple 1 2 3)))
+(assert (= z (tuple 1 2 3)))
 (declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 1)))
+(assert (= zt (tuple 3 2 1)))
 (declare-fun v () (Tuple Int Int Int Int Int Int))
-(assert (= v (mkTuple 1 2 3 3 2 1)))
+(assert (= v (tuple 1 2 3 3 2 1)))
 (assert (member z x))
 (assert (member zt y))
 (assert (not (member v (product x y))))
diff --git a/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_1_1.cvc.smt2
index 696ae31ba..5d8c2dbf2 100644
--- a/test/regress/regress0/rels/rel_product_1_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_product_1_1.cvc.smt2
@@ -7,11 +7,11 @@
 (declare-fun y () (Set (Tuple Int Int Int)))
 (declare-fun r () (Set (Tuple Int Int Int Int Int Int)))
 (declare-fun z () (Tuple Int Int Int))
-(assert (= z (mkTuple 1 2 3)))
+(assert (= z (tuple 1 2 3)))
 (declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 1)))
+(assert (= zt (tuple 3 2 1)))
 (assert (member z x))
 (assert (member zt y))
-(assert (member (mkTuple 1 1 1 1 1 1) r))
+(assert (member (tuple 1 1 1 1 1 1) r))
 (assert (= r (product x y)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2
index 9952b64ec..0c8188f1f 100644
--- a/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2
@@ -7,13 +7,13 @@
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun f () Int)
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple f 3)))
+(assert (= d (tuple f 3)))
 (assert (member d y))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 f)))
+(assert (= e (tuple 4 f)))
 (assert (member e x))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 3)))
+(assert (= a (tuple 4 3)))
 (assert (= r (join x y)))
 (assert (not (member a r)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2
index b677ddb0e..2e10e76ad 100644
--- a/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2
@@ -10,7 +10,7 @@
 (declare-fun a () (Tuple Int Int))
 (assert (member a x))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
 (assert (= r (join x y)))
 (assert (not (member e r)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2
index 21f7c6d89..2615112c2 100644
--- a/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2
@@ -6,12 +6,12 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 1 3)))
-(assert (member (mkTuple 1 3) y))
+(assert (= d (tuple 1 3)))
+(assert (member (tuple 1 3) y))
 (declare-fun a () (Tuple Int Int))
 (assert (member a x))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
 (assert (= r (join x y)))
 (assert (not (member e r)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2
index 7302a53b1..c170fd7a0 100644
--- a/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2
@@ -9,10 +9,10 @@
 (declare-fun d () (Tuple Int Int))
 (assert (member d y))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 f)))
+(assert (= e (tuple 4 f)))
 (assert (member e x))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 3)))
+(assert (= a (tuple 4 3)))
 (assert (= r (join x y)))
 (assert (not (member a r)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tc_11.cvc.smt2 b/test/regress/regress0/rels/rel_tc_11.cvc.smt2
index 0b0cd0d07..5398cf388 100644
--- a/test/regress/regress0/rels/rel_tc_11.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tc_11.cvc.smt2
@@ -6,13 +6,13 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int Int Int)))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 5 3) x))
-(assert (member (mkTuple 3 9) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 5 3) x))
+(assert (member (tuple 3 9) x))
 (assert (= z (product x y)))
-(assert (member (mkTuple 1 2 3 4) z))
-(assert (not (member (mkTuple 5 9) x)))
-(assert (member (mkTuple 3 8) y))
+(assert (member (tuple 1 2 3 4) z))
+(assert (not (member (tuple 5 9) x)))
+(assert (member (tuple 3 8) y))
 (assert (= y (tclosure x)))
-(assert (not (member (mkTuple 1 2) y)))
+(assert (not (member (tuple 1 2) y)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 b/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2
index 689390402..07c60c562 100644
--- a/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2
@@ -6,18 +6,18 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun e () Int)
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 e)))
+(assert (= a (tuple 1 e)))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple e 5)))
+(assert (= d (tuple e 5)))
 (assert (member a x))
 (assert (member d x))
-(assert (not (member (mkTuple 1 1) x)))
-(assert (not (member (mkTuple 1 2) x)))
-(assert (not (member (mkTuple 1 3) x)))
-(assert (not (member (mkTuple 1 4) x)))
-(assert (not (member (mkTuple 1 5) x)))
-(assert (not (member (mkTuple 1 6) x)))
-(assert (not (member (mkTuple 1 7) x)))
+(assert (not (member (tuple 1 1) x)))
+(assert (not (member (tuple 1 2) x)))
+(assert (not (member (tuple 1 3) x)))
+(assert (not (member (tuple 1 4) x)))
+(assert (not (member (tuple 1 5) x)))
+(assert (not (member (tuple 1 6) x)))
+(assert (not (member (tuple 1 7) x)))
 (assert (= y (tclosure x)))
-(assert (member (mkTuple 1 5) y))
+(assert (member (tuple 1 5) y))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tc_3.cvc.smt2 b/test/regress/regress0/rels/rel_tc_3.cvc.smt2
index 46b7cff5b..9af4c2490 100644
--- a/test/regress/regress0/rels/rel_tc_3.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tc_3.cvc.smt2
@@ -8,13 +8,13 @@
 (declare-fun b () Int)
 (declare-fun c () Int)
 (declare-fun d () Int)
-(assert (member (mkTuple 1 a) x))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 1 d) x))
-(assert (member (mkTuple b 1) x))
+(assert (member (tuple 1 a) x))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 1 d) x))
+(assert (member (tuple b 1) x))
 (assert (= b d))
 (assert (> b (- d 1)))
 (assert (< b (+ d 1)))
 (assert (= y (tclosure x)))
-(assert (not (member (mkTuple 1 1) y)))
+(assert (not (member (tuple 1 1) y)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2
index 4d44f31a5..4041735f9 100644
--- a/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2
@@ -8,10 +8,10 @@
 (declare-fun b () Int)
 (declare-fun c () Int)
 (declare-fun d () Int)
-(assert (member (mkTuple 1 a) x))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 1 d) x))
-(assert (member (mkTuple b 1) x))
+(assert (member (tuple 1 a) x))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 1 d) x))
+(assert (member (tuple b 1) x))
 (assert (= b d))
 (assert (= y (tclosure x)))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tc_7.cvc.smt2 b/test/regress/regress0/rels/rel_tc_7.cvc.smt2
index f5abb8eef..b7200a9ef 100644
--- a/test/regress/regress0/rels/rel_tc_7.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tc_7.cvc.smt2
@@ -5,6 +5,6 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (assert (= y (join (tclosure x) x)))
-(assert (member (mkTuple 1 2) (join (join x x) x)))
+(assert (member (tuple 1 2) (join (join x x) x)))
 (assert (not (subset y (tclosure x))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tc_8.cvc.smt2 b/test/regress/regress0/rels/rel_tc_8.cvc.smt2
index 9dc3f9f50..0485a06e9 100644
--- a/test/regress/regress0/rels/rel_tc_8.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tc_8.cvc.smt2
@@ -4,6 +4,6 @@
 
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
-(assert (member (mkTuple 2 2) (tclosure x)))
+(assert (member (tuple 2 2) (tclosure x)))
 (assert (= x (as emptyset (Set (Tuple Int Int)))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2
index 5db2710d8..4e7a33e04 100644
--- a/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2
@@ -5,9 +5,9 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
-(assert (member (mkTuple 1 3) x))
-(assert (or (member (mkTuple 2 3) z) (member (mkTuple 2 1) z)))
+(assert (member (tuple 1 3) x))
+(assert (or (member (tuple 2 3) z) (member (tuple 2 1) z)))
 (assert (= y (transpose x)))
-(assert (not (member (mkTuple 1 2) y)))
+(assert (not (member (tuple 1 2) y)))
 (assert (= x z))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2
index 594e0c52f..05761030c 100644
--- a/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2
@@ -6,21 +6,21 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 5 1)))
+(assert (= a (tuple 5 1)))
 (declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 7 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
+(assert (= b (tuple 7 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
 (assert (member b y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
 (assert (= r (join x y)))
 (assert (member z x))
 (assert (member zt y))
diff --git a/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2
index fe2f9f2db..f1faefaeb 100644
--- a/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2
@@ -7,20 +7,20 @@
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 1 7)))
+(assert (= b (tuple 1 7)))
 (declare-fun c () (Tuple Int Int))
-(assert (= c (mkTuple 2 3)))
+(assert (= c (tuple 2 3)))
 (assert (member b x))
 (assert (member c x))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 7 3)))
+(assert (= d (tuple 7 3)))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 7)))
+(assert (= e (tuple 4 7)))
 (assert (member d y))
 (assert (member e y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 3 4) z))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
 (assert (= r (join (join x y) z)))
 (assert (not (member a (transpose r))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2
index fb402a909..0f3d124ae 100644
--- a/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2
@@ -6,13 +6,13 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
 (assert (= r (join (join (transpose x) y) z)))
 (assert (not (member a (transpose r))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2
index 23c235be6..1443c9ca3 100644
--- a/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2
@@ -7,17 +7,17 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
-(assert (member (mkTuple 3 3) w))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
+(assert (member (tuple 3 3) w))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
 (assert (not (member a (transpose r))))
 (declare-fun zz () (Set (Tuple Int Int)))
 (assert (= zz (join (transpose x) y)))
-(assert (not (member (mkTuple 1 3) w)))
-(assert (not (member (mkTuple 1 3) (union w zz))))
+(assert (not (member (tuple 1 3) w)))
+(assert (not (member (tuple 1 3) (union w zz))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2
index 672844f08..1dcfc0eb6 100644
--- a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2
@@ -6,16 +6,16 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
-(assert (= x (union (singleton (mkTuple 1 7)) (singleton (mkTuple 2 3)))))
+(assert (= x (union (singleton (tuple 1 7)) (singleton (tuple 2 3)))))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 7 3)))
+(assert (= d (tuple 7 3)))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 7)))
+(assert (= e (tuple 4 7)))
 (assert (member d y))
 (assert (member e y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 3 4) z))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
 (assert (= r (join (join x y) z)))
 (assert (not (member a (transpose r))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2
index 83b6ab904..82f6a0238 100644
--- a/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2
@@ -11,9 +11,9 @@
 (declare-fun u () Int)
 (assert (and (< 4 t) (< t 6)))
 (assert (and (< 4 u) (< u 6)))
-(assert (member (mkTuple 1 u) x))
-(assert (member (mkTuple t 3) y))
+(assert (member (tuple 1 u) x))
+(assert (member (tuple t 3) y))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 3)))
+(assert (= a (tuple 1 3)))
 (assert (not (member a (join x y))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2
index f3bcad8a1..d7d89d3a4 100644
--- a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2
@@ -7,13 +7,13 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int Int Int)))
-(assert (member (mkTuple 2 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 2 2) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 2 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 2 2) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
 (declare-fun v () (Tuple Int Int Int Int))
-(assert (= v (mkTuple 4 3 2 1)))
+(assert (= v (tuple 4 3 2 1)))
 (assert (= r (product (join (transpose x) y) z)))
 (assert (not (member v (transpose r))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2
index 0fee2c136..80b359e8b 100644
--- a/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2
@@ -11,10 +11,10 @@
 (declare-fun u () Int)
 (assert (and (< 4 t) (< t 6)))
 (assert (and (< 4 u) (< u 6)))
-(assert (member (mkTuple 1 t) x))
-(assert (member (mkTuple u 3) y))
+(assert (member (tuple 1 t) x))
+(assert (member (tuple u 3) y))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 3)))
+(assert (= a (tuple 1 3)))
 (assert (not (member a (join x y))))
 (declare-fun st () (Set Int))
 (declare-fun su () (Set Int))
diff --git a/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_0.cvc.smt2
index 9996209b8..280f78ea2 100644
--- a/test/regress/regress0/rels/rel_transpose_0.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_0.cvc.smt2
@@ -6,9 +6,9 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun a () Int)
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (assert (member z x))
 (assert (not (member zt (transpose x))))
 (assert (= y (transpose x)))
diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_1.cvc.smt2
index 3d21e17a9..fb7070e82 100644
--- a/test/regress/regress0/rels/rel_transpose_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_1.cvc.smt2
@@ -5,9 +5,9 @@
 (declare-fun x () (Set (Tuple Int Int Int)))
 (declare-fun y () (Set (Tuple Int Int Int)))
 (declare-fun z () (Tuple Int Int Int))
-(assert (= z (mkTuple 1 2 3)))
+(assert (= z (tuple 1 2 3)))
 (declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 1)))
+(assert (= zt (tuple 3 2 1)))
 (assert (member z x))
 (assert (not (member zt (transpose x))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2
index d54b8c608..0d9f6d028 100644
--- a/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2
@@ -6,9 +6,9 @@
 (declare-fun y () (Set (Tuple Int Int Int)))
 (declare-fun z () (Tuple Int Int Int))
 (declare-fun a () Int)
-(assert (= z (mkTuple 1 2 a)))
+(assert (= z (tuple 1 2 a)))
 (declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 2)))
+(assert (= zt (tuple 3 2 2)))
 (assert (member z x))
 (assert (member zt (transpose x)))
 (assert (= y (transpose x)))
diff --git a/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_3.cvc.smt2
index 3109186f1..ea737919e 100644
--- a/test/regress/regress0/rels/rel_transpose_3.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_3.cvc.smt2
@@ -5,9 +5,9 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (assert (= x y))
 (assert (member z x))
 (assert (not (member zt (transpose y))))
diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_4.cvc.smt2
index d75d64b64..5ba3cc2c6 100644
--- a/test/regress/regress0/rels/rel_transpose_4.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_4.cvc.smt2
@@ -5,7 +5,7 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (assert (member z x))
-(assert (not (member (mkTuple 2 1) (transpose x))))
+(assert (not (member (tuple 2 1) (transpose x))))
 (check-sat)
diff --git a/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_5.cvc.smt2
index 927a5f07f..8a58ca763 100644
--- a/test/regress/regress0/rels/rel_transpose_5.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_5.cvc.smt2
@@ -6,12 +6,12 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (assert (member zt y))
 (declare-fun w () (Tuple Int Int))
-(assert (= w (mkTuple 2 2)))
+(assert (= w (tuple 2 2)))
 (assert (member w y))
 (assert (member z x))
 (assert (not (member zt (transpose (join x y)))))
diff --git a/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_6.cvc.smt2
index 7c097fc46..1dc932a81 100644
--- a/test/regress/regress0/rels/rel_transpose_6.cvc.smt2
+++ b/test/regress/regress0/rels/rel_transpose_6.cvc.smt2
@@ -5,13 +5,13 @@
 (declare-fun x () (Set (Tuple Int Int)))
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (assert (member z x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 3 5) x))
-(assert (member (mkTuple 3 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 3 5) x))
+(assert (member (tuple 3 3) x))
 (assert (= x (transpose y)))
 (assert (not (member zt y)))
 (assert (member z y))
diff --git a/test/regress/regress0/rels/relations-ops.smt2 b/test/regress/regress0/rels/relations-ops.smt2
index abb7faf10..e68eb49bb 100644
--- a/test/regress/regress0/rels/relations-ops.smt2
+++ b/test/regress/regress0/rels/relations-ops.smt2
@@ -11,12 +11,12 @@
 (declare-fun lt2 () (Set (Tuple Int Int)))
 (declare-fun i () Int)
 
-(assert (= r1 (insert (mkTuple "a" 1) (mkTuple "b" 2) (mkTuple "c" 3) (singleton (mkTuple "d" 4)))))
-(assert (= r2 (insert (mkTuple 1 "1") (mkTuple 2 "2") (mkTuple 3 "3") (singleton (mkTuple 17 "17")))))
+(assert (= r1 (insert (tuple "a" 1) (tuple "b" 2) (tuple "c" 3) (singleton (tuple "d" 4)))))
+(assert (= r2 (insert (tuple 1 "1") (tuple 2 "2") (tuple 3 "3") (singleton (tuple 17 "17")))))
 (assert (= r (join r1 r2)))
 (assert (= s (transpose r)))
 (assert (= t (product r1 r2)))
-(assert (= lt1 (insert (mkTuple 1 2) (mkTuple 2 3) (mkTuple 3 4) (singleton (mkTuple 4 5)))))
+(assert (= lt1 (insert (tuple 1 2) (tuple 2 3) (tuple 3 4) (singleton (tuple 4 5)))))
 (assert (= lt2 (tclosure lt1)))
 (assert (= i (card t)))
 
diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 b/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2
index dff78fbd8..2ba92270a 100644
--- a/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2
+++ b/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2
@@ -6,7 +6,7 @@
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun x () Int)
 (declare-fun y () Int)
-(assert (member (mkTuple 1 x) w))
-(assert (member (mkTuple y 2) z))
-(assert (not (member (mkTuple 1 2) (join w z))))
+(assert (member (tuple 1 x) w))
+(assert (member (tuple y 2) z))
+(assert (not (member (tuple 1 2) (join w z))))
 (check-sat)
diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2
index 3e7239774..b81843871 100644
--- a/test/regress/regress0/sets/complement3.cvc.smt2
+++ b/test/regress/regress0/sets/complement3.cvc.smt2
@@ -9,8 +9,8 @@
 (declare-fun ATOM_UNIV () (Set (Tuple Atom)))
 (declare-fun V1 () Atom)
 (assert (= C32 (intersection (complement C2) (complement C4))))
-(assert (member (mkTuple V1) (complement C32)))
+(assert (member (tuple V1) (complement C32)))
 (assert (= ATOM_UNIV (as univset (Set (Tuple Atom)))))
-(assert (member (mkTuple V1) ATOM_UNIV))
-(assert (member (mkTuple V1) (complement C2)))
+(assert (member (tuple V1) ATOM_UNIV))
+(assert (member (tuple V1) (complement C2)))
 (check-sat)
diff --git a/test/regress/regress1/datatypes/tuple_projection.smt2 b/test/regress/regress1/datatypes/tuple_projection.smt2
index bdd9d5458..dfe37a9d0 100644
--- a/test/regress/regress1/datatypes/tuple_projection.smt2
+++ b/test/regress/regress1/datatypes/tuple_projection.smt2
@@ -4,8 +4,8 @@
 (declare-fun u () (Tuple String String))
 (declare-fun v () Tuple)
 (declare-fun x () String)
-(assert (= t (mkTuple "a" "b" "c" "d")))
-(assert (= x ((_ tupSel 0) t)))
+(assert (= t (tuple "a" "b" "c" "d")))
+(assert (= x ((_ tuple_select 0) t)))
 (assert (= u ((_ tuple_project 2 3) t)))
 (assert (= v (tuple_project t)))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
index b099c7914..433c1f102 100644
--- a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
+++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
@@ -27,5 +27,5 @@
 (declare-fun ev_set () (Set |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|))
 (assert (= ev_set (union (singleton ow1) (singleton or2))))
 (declare-fun RF () (Set (Tuple |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)))
-(assert (forall ((r |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|) (w |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (=> (and (member r ev_set) (member w ev_set)) (= (member (mkTuple r w) RF) (and (= (O r) R) (= (O w) W))))))
+(assert (forall ((r |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|) (w |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (=> (and (member r ev_set) (member w ev_set)) (= (member (tuple r w) RF) (and (= (O r) R) (= (O w) W))))))
 (check-sat)
diff --git a/test/regress/regress1/rels/addr_book_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1.cvc.smt2
index 7a6ac7d5b..591303875 100644
--- a/test/regress/regress1/rels/addr_book_1.cvc.smt2
+++ b/test/regress/regress1/rels/addr_book_1.cvc.smt2
@@ -13,26 +13,26 @@
 (declare-fun addr () (Set (Tuple Atom Atom Atom)))
 (declare-fun b1 () Atom)
 (declare-fun b1_tup () (Tuple Atom))
-(assert (= b1_tup (mkTuple b1)))
+(assert (= b1_tup (tuple b1)))
 (assert (member b1_tup Book))
 (declare-fun b2 () Atom)
 (declare-fun b2_tup () (Tuple Atom))
-(assert (= b2_tup (mkTuple b2)))
+(assert (= b2_tup (tuple b2)))
 (assert (member b2_tup Book))
 (declare-fun b3 () Atom)
 (declare-fun b3_tup () (Tuple Atom))
-(assert (= b3_tup (mkTuple b3)))
+(assert (= b3_tup (tuple b3)))
 (assert (member b3_tup Book))
 (declare-fun m () Atom)
 (declare-fun m_tup () (Tuple Atom))
-(assert (= m_tup (mkTuple m)))
+(assert (= m_tup (tuple m)))
 (assert (member m_tup Name))
 (declare-fun t () Atom)
 (declare-fun t_tup () (Tuple Atom))
-(assert (= t_tup (mkTuple t)))
+(assert (= t_tup (tuple t)))
 (assert (member t_tup Target))
 (assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom)))))
-(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t)))))
-(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t)))))
+(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (tuple m t)))))
+(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (tuple m t)))))
 (assert (not (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr))))
 (check-sat)
diff --git a/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1_1.cvc.smt2
index 29eb2106d..a7cfcaf38 100644
--- a/test/regress/regress1/rels/addr_book_1_1.cvc.smt2
+++ b/test/regress/regress1/rels/addr_book_1_1.cvc.smt2
@@ -13,26 +13,26 @@
 (declare-fun addr () (Set (Tuple Atom Atom Atom)))
 (declare-fun b1 () Atom)
 (declare-fun b1_tup () (Tuple Atom))
-(assert (= b1_tup (mkTuple b1)))
+(assert (= b1_tup (tuple b1)))
 (assert (member b1_tup Book))
 (declare-fun b2 () Atom)
 (declare-fun b2_tup () (Tuple Atom))
-(assert (= b2_tup (mkTuple b2)))
+(assert (= b2_tup (tuple b2)))
 (assert (member b2_tup Book))
 (declare-fun b3 () Atom)
 (declare-fun b3_tup () (Tuple Atom))
-(assert (= b3_tup (mkTuple b3)))
+(assert (= b3_tup (tuple b3)))
 (assert (member b3_tup Book))
 (declare-fun m () Atom)
 (declare-fun m_tup () (Tuple Atom))
-(assert (= m_tup (mkTuple m)))
+(assert (= m_tup (tuple m)))
 (assert (member m_tup Name))
 (declare-fun t () Atom)
 (declare-fun t_tup () (Tuple Atom))
-(assert (= t_tup (mkTuple t)))
+(assert (= t_tup (tuple t)))
 (assert (member t_tup Target))
 (assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom)))))
-(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t)))))
-(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t)))))
+(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (tuple m t)))))
+(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (tuple m t)))))
 (assert (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr)))
 (check-sat)
diff --git a/test/regress/regress1/rels/bv1-unit.cvc.smt2 b/test/regress/regress1/rels/bv1-unit.cvc.smt2
index b61b9403f..ba4dac386 100644
--- a/test/regress/regress1/rels/bv1-unit.cvc.smt2
+++ b/test/regress/regress1/rels/bv1-unit.cvc.smt2
@@ -11,8 +11,8 @@
 (declare-fun d () (_ BitVec 1))
 (declare-fun e () (_ BitVec 1))
 (assert (not (= b c)))
-(assert (member (mkTuple a u b) x))
-(assert (member (mkTuple a u c) x))
-(assert (member (mkTuple d u a) y))
-(assert (not (member (mkTuple a u u a) (join x y))))
+(assert (member (tuple a u b) x))
+(assert (member (tuple a u c) x))
+(assert (member (tuple d u a) y))
+(assert (not (member (tuple a u u a) (join x y))))
 (check-sat)
diff --git a/test/regress/regress1/rels/bv1-unitb.cvc.smt2 b/test/regress/regress1/rels/bv1-unitb.cvc.smt2
index c1db4195f..696c8919e 100644
--- a/test/regress/regress1/rels/bv1-unitb.cvc.smt2
+++ b/test/regress/regress1/rels/bv1-unitb.cvc.smt2
@@ -12,8 +12,8 @@
 (declare-fun e () (_ BitVec 1))
 (declare-fun u () unitb)
 (assert (not (= b c)))
-(assert (member (mkTuple a u b) x))
-(assert (member (mkTuple a u c) x))
-(assert (member (mkTuple d u a) y))
-(assert (not (member (mkTuple a u u a) (join x y))))
+(assert (member (tuple a u b) x))
+(assert (member (tuple a u c) x))
+(assert (member (tuple d u a) y))
+(assert (not (member (tuple a u u a) (join x y))))
 (check-sat)
diff --git a/test/regress/regress1/rels/bv1.cvc.smt2 b/test/regress/regress1/rels/bv1.cvc.smt2
index 93fa6a296..1df5ee38b 100644
--- a/test/regress/regress1/rels/bv1.cvc.smt2
+++ b/test/regress/regress1/rels/bv1.cvc.smt2
@@ -10,8 +10,8 @@
 (declare-fun d () (_ BitVec 1))
 (declare-fun e () (_ BitVec 1))
 (assert (not (= b c)))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple a c) x))
-(assert (member (mkTuple d a) y))
-(assert (not (member (mkTuple a a) (join x y))))
+(assert (member (tuple a b) x))
+(assert (member (tuple a c) x))
+(assert (member (tuple d a) y))
+(assert (not (member (tuple a a) (join x y))))
 (check-sat)
diff --git a/test/regress/regress1/rels/bv2.cvc.smt2 b/test/regress/regress1/rels/bv2.cvc.smt2
index 824e7e125..005737b36 100644
--- a/test/regress/regress1/rels/bv2.cvc.smt2
+++ b/test/regress/regress1/rels/bv2.cvc.smt2
@@ -10,8 +10,8 @@
 (declare-fun d () (_ BitVec 2))
 (declare-fun e () (_ BitVec 2))
 (assert (not (= b c)))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple a c) x))
-(assert (member (mkTuple d a) y))
-(assert (not (member (mkTuple a a) (join x y))))
+(assert (member (tuple a b) x))
+(assert (member (tuple a c) x))
+(assert (member (tuple d a) y))
+(assert (not (member (tuple a a) (join x y))))
 (check-sat)
diff --git a/test/regress/regress1/rels/garbage_collect.cvc.smt2 b/test/regress/regress1/rels/garbage_collect.cvc.smt2
index c4bba2cd3..55f181acd 100644
--- a/test/regress/regress1/rels/garbage_collect.cvc.smt2
+++ b/test/regress/regress1/rels/garbage_collect.cvc.smt2
@@ -16,10 +16,10 @@
 (declare-fun s1 () H_TYPE)
 (declare-fun s2 () H_TYPE)
 (declare-fun s3 () H_TYPE)
-(assert (= h0 (singleton (mkTuple s0))))
-(assert (= h1 (singleton (mkTuple s1))))
-(assert (= h2 (singleton (mkTuple s2))))
-(assert (= h3 (singleton (mkTuple s3))))
+(assert (= h0 (singleton (tuple s0))))
+(assert (= h1 (singleton (tuple s1))))
+(assert (= h2 (singleton (tuple s2))))
+(assert (= h3 (singleton (tuple s3))))
 (declare-fun ref () (Set (Tuple H_TYPE Obj Obj)))
 (declare-fun mark () (Set (Tuple H_TYPE Obj)))
 (declare-fun empty_obj_set () (Set (Tuple Obj)))
@@ -28,10 +28,10 @@
 (declare-fun live () Obj)
 (assert (= (join h1 mark) empty_obj_set))
 (assert (subset (join h0 ref) (join h1 ref)))
-(assert (forall ((n Obj)) (=> (member (mkTuple root n) (tclosure (join h1 ref))) (member (mkTuple n) (join h2 mark)))))
+(assert (forall ((n Obj)) (=> (member (tuple root n) (tclosure (join h1 ref))) (member (tuple n) (join h2 mark)))))
 (assert (subset (join h1 ref) (join h2 ref)))
-(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set)))))
-(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref))))))))
-(assert (member (mkTuple root live) (tclosure (join h0 ref))))
-(assert (let ((_let_1 (singleton (mkTuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref))))))
+(assert (forall ((n Obj)) (let ((_let_1 (tuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set)))))
+(assert (forall ((n Obj)) (let ((_let_1 (tuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref))))))))
+(assert (member (tuple root live) (tclosure (join h0 ref))))
+(assert (let ((_let_1 (singleton (tuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref))))))
 (check-sat)
diff --git a/test/regress/regress1/rels/iden_1_1.cvc.smt2 b/test/regress/regress1/rels/iden_1_1.cvc.smt2
index eb09d698f..305476798 100644
--- a/test/regress/regress1/rels/iden_1_1.cvc.smt2
+++ b/test/regress/regress1/rels/iden_1_1.cvc.smt2
@@ -15,8 +15,8 @@
 (assert (= univ (as univset (Set (Tuple Atom)))))
 (assert (= univ2 (as univset (Set (Tuple Atom Atom)))))
 (assert (= univ2 (product univ univ)))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple c d) x))
+(assert (member (tuple a b) x))
+(assert (member (tuple c d) x))
 (assert (not (= a b)))
 (assert (subset (iden univ) x))
 (check-sat)
diff --git a/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2
index 1eb1419c8..60696f706 100644
--- a/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2
+++ b/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2
@@ -10,12 +10,12 @@
 (declare-fun w () (Set (Tuple Int unit)))
 (declare-fun z () (Set (Tuple unit Int)))
 (assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (and (= _let_2 _let_1) (= _let_2 (transpose _let_1))))))
-(assert (member (mkTuple 0 1) (join x y)))
+(assert (member (tuple 0 1) (join x y)))
 (declare-fun t () Int)
 (assert (and (>= t 0) (<= t 1)))
 (declare-fun s () Int)
 (assert (and (>= s 0) (<= s 1)))
 (assert (= (+ s t) 1))
-(assert (member (mkTuple s u) w))
-(assert (not (member (mkTuple u t) z)))
+(assert (member (tuple s u) w))
+(assert (not (member (tuple u t) z)))
 (check-sat)
diff --git a/test/regress/regress1/rels/join-eq-structure.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure.cvc.smt2
index 5144ac4c2..0e510c77a 100644
--- a/test/regress/regress1/rels/join-eq-structure.cvc.smt2
+++ b/test/regress/regress1/rels/join-eq-structure.cvc.smt2
@@ -10,12 +10,12 @@
 (declare-fun w () (Set (Tuple Int unit)))
 (declare-fun z () (Set (Tuple unit Int)))
 (assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (or (= _let_2 _let_1) (= _let_2 (transpose _let_1))))))
-(assert (member (mkTuple 0 1) (join x y)))
+(assert (member (tuple 0 1) (join x y)))
 (declare-fun t () Int)
 (assert (and (>= t 0) (<= t 1)))
 (declare-fun s () Int)
 (assert (and (>= s 0) (<= s 1)))
 (assert (= (+ s t) 1))
-(assert (member (mkTuple s u) w))
-(assert (not (member (mkTuple u t) z)))
+(assert (member (tuple s u) w))
+(assert (not (member (tuple u t) z)))
 (check-sat)
diff --git a/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_0_1.cvc.smt2
index 8a28b74ae..ae33348bd 100644
--- a/test/regress/regress1/rels/joinImg_0_1.cvc.smt2
+++ b/test/regress/regress1/rels/joinImg_0_1.cvc.smt2
@@ -9,20 +9,20 @@
 (declare-fun t () (Set (Tuple Int)))
 (declare-fun u () (Set (Tuple Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
+(assert (= a (tuple 1 5)))
 (declare-fun b () Int)
-(assert (member (mkTuple 1 7) x))
+(assert (member (tuple 1 7) x))
 (assert (member z x))
-(assert (member (mkTuple 7 5) y))
+(assert (member (tuple 7 5) y))
 (assert (= t (join_image x 2)))
-(assert (member (mkTuple 3) (join_image x 2)))
+(assert (member (tuple 3) (join_image x 2)))
 (assert (= u (join_image x 1)))
-(assert (member (mkTuple 4) (join_image x 2)))
-(assert (member (mkTuple b) (join_image x 1)))
+(assert (member (tuple 4) (join_image x 2)))
+(assert (member (tuple b) (join_image x 1)))
 (check-sat)
diff --git a/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 b/test/regress/regress1/rels/joinImg_0_2.cvc.smt2
index 8f1954c10..86fc76670 100644
--- a/test/regress/regress1/rels/joinImg_0_2.cvc.smt2
+++ b/test/regress/regress1/rels/joinImg_0_2.cvc.smt2
@@ -10,22 +10,22 @@
 (declare-fun u () (Set (Tuple Int)))
 (declare-fun univ () (Set (Tuple Int)))
 (declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
 (declare-fun s () (Tuple Int Int))
-(assert (= s (mkTuple 1 1)))
+(assert (= s (tuple 1 1)))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
+(assert (= a (tuple 1 5)))
 (declare-fun b () Int)
-(assert (member (mkTuple 1 7) x))
+(assert (member (tuple 1 7) x))
 (assert (member z x))
-(assert (member (mkTuple 7 5) y))
+(assert (member (tuple 7 5) y))
 (assert (= t (join_image x 2)))
 (assert (= univ (join_image x 0)))
-(assert (member (mkTuple 100) t))
-(assert (not (member (mkTuple 3) univ)))
+(assert (member (tuple 100) t))
+(assert (not (member (tuple 3) univ)))
 (assert (= u (join_image x 1)))
-(assert (member (mkTuple 4) (join_image x 2)))
-(assert (member (mkTuple b) (join_image x 1)))
+(assert (member (tuple 4) (join_image x 2)))
+(assert (member (tuple b) (join_image x 1)))
 (check-sat)
diff --git a/test/regress/regress1/rels/joinImg_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1.cvc.smt2
index 3c5664d76..4d7c56000 100644
--- a/test/regress/regress1/rels/joinImg_1.cvc.smt2
+++ b/test/regress/regress1/rels/joinImg_1.cvc.smt2
@@ -12,7 +12,7 @@
 (declare-fun c () Atom)
 (declare-fun d () Atom)
 (declare-fun e () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
-(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
+(assert (member (tuple a) (join_image x 2)))
+(assert (= x (union (union (singleton (tuple b c)) (singleton (tuple d e))) (singleton (tuple c e)))))
 (assert (not (= a b)))
 (check-sat)
diff --git a/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1_1.cvc.smt2
index c8e228f1b..dc940a43b 100644
--- a/test/regress/regress1/rels/joinImg_1_1.cvc.smt2
+++ b/test/regress/regress1/rels/joinImg_1_1.cvc.smt2
@@ -12,8 +12,8 @@
 (declare-fun c () Atom)
 (declare-fun d () Atom)
 (declare-fun e () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
+(assert (member (tuple a) (join_image x 2)))
 (assert (= t (join_image x 2)))
-(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
-(assert (member (mkTuple c) t))
+(assert (= x (union (union (singleton (tuple b c)) (singleton (tuple d e))) (singleton (tuple c e)))))
+(assert (member (tuple c) t))
 (check-sat)
diff --git a/test/regress/regress1/rels/joinImg_2.cvc.smt2 b/test/regress/regress1/rels/joinImg_2.cvc.smt2
index 9f8efdfff..527770994 100644
--- a/test/regress/regress1/rels/joinImg_2.cvc.smt2
+++ b/test/regress/regress1/rels/joinImg_2.cvc.smt2
@@ -14,13 +14,13 @@
 (declare-fun e () Atom)
 (declare-fun f () Atom)
 (declare-fun g () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
-(assert (member (mkTuple a) (join_image y 3)))
-(assert (= x (union (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))) (singleton (mkTuple f b)))))
-(assert (member (mkTuple a f) x))
-(assert (member (mkTuple a f) y))
+(assert (member (tuple a) (join_image x 2)))
+(assert (member (tuple a) (join_image y 3)))
+(assert (= x (union (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e))) (singleton (tuple f b)))))
+(assert (member (tuple a f) x))
+(assert (member (tuple a f) y))
 (assert (= x y))
 (assert (not (= a b)))
-(assert (not (member (mkTuple d) (join_image x 2))))
+(assert (not (member (tuple d) (join_image x 2))))
 (assert (= f d))
 (check-sat)
diff --git a/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_2_1.cvc.smt2
index 797e7b35b..0d563415b 100644
--- a/test/regress/regress1/rels/joinImg_2_1.cvc.smt2
+++ b/test/regress/regress1/rels/joinImg_2_1.cvc.smt2
@@ -14,9 +14,9 @@
 (declare-fun e () Atom)
 (declare-fun f () Atom)
 (declare-fun g () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
-(assert (member (mkTuple a) (join_image y 1)))
-(assert (= y (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
-(assert (= x (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
+(assert (member (tuple a) (join_image x 2)))
+(assert (member (tuple a) (join_image y 1)))
+(assert (= y (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e)))))
+(assert (= x (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e)))))
 (assert (or (not (= a b)) (not (= a f))))
 (check-sat)
diff --git a/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 b/test/regress/regress1/rels/prod-mod-eq.cvc.smt2
index 7d9147a8b..088976c2b 100644
--- a/test/regress/regress1/rels/prod-mod-eq.cvc.smt2
+++ b/test/regress/regress1/rels/prod-mod-eq.cvc.smt2
@@ -11,10 +11,10 @@
 (declare-fun z2 () (Set (Tuple Int Int)))
 (declare-fun w2 () (Set (Tuple Int Int)))
 (assert (not (= z (product x y))))
-(assert (member (mkTuple 0 1 2 3) z))
-(assert (member (mkTuple 0 1) z1))
-(assert (member (mkTuple 0 1) z2))
-(assert (member (mkTuple 2 3) w1))
-(assert (member (mkTuple 2 3) w2))
+(assert (member (tuple 0 1 2 3) z))
+(assert (member (tuple 0 1) z1))
+(assert (member (tuple 0 1) z2))
+(assert (member (tuple 2 3) w1))
+(assert (member (tuple 2 3) w2))
 (assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2))))
 (check-sat)
diff --git a/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 b/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2
index b2bee8b3f..e54259778 100644
--- a/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2
+++ b/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2
@@ -13,10 +13,10 @@
 (declare-fun P ((Set (Tuple Int Int Int Int))) Bool)
 (assert (= z (product x y)))
 (assert (P z))
-(assert (not (P (singleton (mkTuple 0 1 2 3)))))
-(assert (member (mkTuple 0 1) z1))
-(assert (member (mkTuple 0 1) z2))
-(assert (member (mkTuple 2 3) w1))
-(assert (member (mkTuple 2 3) w2))
+(assert (not (P (singleton (tuple 0 1 2 3)))))
+(assert (member (tuple 0 1) z1))
+(assert (member (tuple 0 1) z2))
+(assert (member (tuple 2 3) w1))
+(assert (member (tuple 2 3) w2))
 (assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2))))
 (check-sat)
diff --git a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2
index ccd152268..7955cf532 100644
--- a/test/regress/regress1/rels/rel_complex_3.cvc.smt2
+++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2
@@ -8,13 +8,13 @@
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun w () (Set (Tuple Int Int)))
 (declare-fun f () (Tuple Int Int))
-(assert (= f (mkTuple 3 1)))
+(assert (= f (tuple 3 1)))
 (assert (member f x))
 (declare-fun g () (Tuple Int Int))
-(assert (= g (mkTuple 1 3)))
+(assert (= g (tuple 1 3)))
 (assert (member g y))
 (declare-fun h () (Tuple Int Int))
-(assert (= h (mkTuple 3 5)))
+(assert (= h (tuple 3 5)))
 (assert (member h x))
 (assert (member h y))
 (assert (= r (join x y)))
diff --git a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2
index 1f99668ac..865105a1b 100644
--- a/test/regress/regress1/rels/rel_complex_4.cvc.smt2
+++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2
@@ -8,19 +8,19 @@
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun w () (Set (Tuple Int Int)))
 (declare-fun f () (Tuple Int Int))
-(assert (= f (mkTuple 3 1)))
+(assert (= f (tuple 3 1)))
 (assert (member f x))
 (declare-fun g () (Tuple Int Int))
-(assert (= g (mkTuple 1 3)))
+(assert (= g (tuple 1 3)))
 (assert (member g y))
 (declare-fun h () (Tuple Int Int))
-(assert (= h (mkTuple 3 5)))
+(assert (= h (tuple 3 5)))
 (assert (member h x))
 (assert (member h y))
 (assert (= r (join x y)))
 (declare-fun a () Int)
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple a a)))
+(assert (= e (tuple a a)))
 (assert (= w (singleton e)))
 (assert (subset (transpose w) y))
 (assert (not (member e r)))
diff --git a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2
index dfbc23c8e..69ec8046e 100644
--- a/test/regress/regress1/rels/rel_complex_5.cvc.smt2
+++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2
@@ -9,20 +9,20 @@
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun w () (Set (Tuple Int Int)))
 (declare-fun f () (Tuple Int Int))
-(assert (= f (mkTuple 3 1)))
+(assert (= f (tuple 3 1)))
 (assert (member f x))
 (declare-fun g () (Tuple Int Int))
-(assert (= g (mkTuple 1 3)))
+(assert (= g (tuple 1 3)))
 (assert (member g y))
 (declare-fun h () (Tuple Int Int))
-(assert (= h (mkTuple 3 5)))
+(assert (= h (tuple 3 5)))
 (assert (member h x))
 (assert (member h y))
 (assert (= r (join x y)))
 (declare-fun a () (Tuple Int))
-(assert (= a (mkTuple 1)))
+(assert (= a (tuple 1)))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 1 1)))
+(assert (= e (tuple 1 1)))
 (assert (let ((_let_1 (singleton a))) (= w (product _let_1 _let_1))))
 (assert (subset (transpose w) y))
 (assert (not (member e r)))
diff --git a/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 b/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2
index 08323ed5a..79cfc078f 100644
--- a/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2
+++ b/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2
@@ -10,12 +10,12 @@
 (declare-fun z () (Set (Tuple Int)))
 (declare-fun r2 () (Set (Tuple Int Int)))
 (declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 1 3)))
-(assert (member (mkTuple 1 3) y))
+(assert (= d (tuple 1 3)))
+(assert (member (tuple 1 3) y))
 (declare-fun a () (Tuple Int Int))
 (assert (member a x))
 (declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
 (assert (= r (join x y)))
 (assert (= r2 (product w z)))
 (assert (not (member e r)))
diff --git a/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 b/test/regress/regress1/rels/rel_pressure_0.cvc.smt2
index 698f2f5d9..d56f72e77 100644
--- a/test/regress/regress1/rels/rel_pressure_0.cvc.smt2
+++ b/test/regress/regress1/rels/rel_pressure_0.cvc.smt2
@@ -7,608 +7,608 @@
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
 (declare-fun a11 () (Tuple Int Int))
-(assert (= a11 (mkTuple 1 1)))
+(assert (= a11 (tuple 1 1)))
 (assert (member a11 x))
 (declare-fun a12 () (Tuple Int Int))
-(assert (= a12 (mkTuple 1 2)))
+(assert (= a12 (tuple 1 2)))
 (assert (member a12 x))
 (declare-fun a13 () (Tuple Int Int))
-(assert (= a13 (mkTuple 1 3)))
+(assert (= a13 (tuple 1 3)))
 (assert (member a13 x))
 (declare-fun a14 () (Tuple Int Int))
-(assert (= a14 (mkTuple 1 4)))
+(assert (= a14 (tuple 1 4)))
 (assert (member a14 x))
 (declare-fun a15 () (Tuple Int Int))
-(assert (= a15 (mkTuple 1 5)))
+(assert (= a15 (tuple 1 5)))
 (assert (member a15 x))
 (declare-fun a16 () (Tuple Int Int))
-(assert (= a16 (mkTuple 1 6)))
+(assert (= a16 (tuple 1 6)))
 (assert (member a16 x))
 (declare-fun a17 () (Tuple Int Int))
-(assert (= a17 (mkTuple 1 7)))
+(assert (= a17 (tuple 1 7)))
 (assert (member a17 x))
 (declare-fun a18 () (Tuple Int Int))
-(assert (= a18 (mkTuple 1 8)))
+(assert (= a18 (tuple 1 8)))
 (assert (member a18 x))
 (declare-fun a19 () (Tuple Int Int))
-(assert (= a19 (mkTuple 1 9)))
+(assert (= a19 (tuple 1 9)))
 (assert (member a19 x))
 (declare-fun a110 () (Tuple Int Int))
-(assert (= a110 (mkTuple 1 10)))
+(assert (= a110 (tuple 1 10)))
 (assert (member a110 x))
 (declare-fun a21 () (Tuple Int Int))
-(assert (= a21 (mkTuple 2 1)))
+(assert (= a21 (tuple 2 1)))
 (assert (member a21 x))
 (declare-fun a22 () (Tuple Int Int))
-(assert (= a22 (mkTuple 2 2)))
+(assert (= a22 (tuple 2 2)))
 (assert (member a22 x))
 (declare-fun a23 () (Tuple Int Int))
-(assert (= a23 (mkTuple 2 3)))
+(assert (= a23 (tuple 2 3)))
 (assert (member a23 x))
 (declare-fun a24 () (Tuple Int Int))
-(assert (= a24 (mkTuple 2 4)))
+(assert (= a24 (tuple 2 4)))
 (assert (member a24 x))
 (declare-fun a25 () (Tuple Int Int))
-(assert (= a25 (mkTuple 2 5)))
+(assert (= a25 (tuple 2 5)))
 (assert (member a25 x))
 (declare-fun a26 () (Tuple Int Int))
-(assert (= a26 (mkTuple 2 6)))
+(assert (= a26 (tuple 2 6)))
 (assert (member a26 x))
 (declare-fun a27 () (Tuple Int Int))
-(assert (= a27 (mkTuple 2 7)))
+(assert (= a27 (tuple 2 7)))
 (assert (member a27 x))
 (declare-fun a28 () (Tuple Int Int))
-(assert (= a28 (mkTuple 2 8)))
+(assert (= a28 (tuple 2 8)))
 (assert (member a28 x))
 (declare-fun a29 () (Tuple Int Int))
-(assert (= a29 (mkTuple 2 9)))
+(assert (= a29 (tuple 2 9)))
 (assert (member a29 x))
 (declare-fun a210 () (Tuple Int Int))
-(assert (= a210 (mkTuple 2 10)))
+(assert (= a210 (tuple 2 10)))
 (assert (member a210 x))
 (declare-fun a31 () (Tuple Int Int))
-(assert (= a31 (mkTuple 3 1)))
+(assert (= a31 (tuple 3 1)))
 (assert (member a31 x))
 (declare-fun a32 () (Tuple Int Int))
-(assert (= a32 (mkTuple 3 2)))
+(assert (= a32 (tuple 3 2)))
 (assert (member a32 x))
 (declare-fun a33 () (Tuple Int Int))
-(assert (= a33 (mkTuple 3 3)))
+(assert (= a33 (tuple 3 3)))
 (assert (member a33 x))
 (declare-fun a34 () (Tuple Int Int))
-(assert (= a34 (mkTuple 3 4)))
+(assert (= a34 (tuple 3 4)))
 (assert (member a34 x))
 (declare-fun a35 () (Tuple Int Int))
-(assert (= a35 (mkTuple 3 5)))
+(assert (= a35 (tuple 3 5)))
 (assert (member a35 x))
 (declare-fun a36 () (Tuple Int Int))
-(assert (= a36 (mkTuple 3 6)))
+(assert (= a36 (tuple 3 6)))
 (assert (member a36 x))
 (declare-fun a37 () (Tuple Int Int))
-(assert (= a37 (mkTuple 3 7)))
+(assert (= a37 (tuple 3 7)))
 (assert (member a37 x))
 (declare-fun a38 () (Tuple Int Int))
-(assert (= a38 (mkTuple 3 8)))
+(assert (= a38 (tuple 3 8)))
 (assert (member a38 x))
 (declare-fun a39 () (Tuple Int Int))
-(assert (= a39 (mkTuple 3 9)))
+(assert (= a39 (tuple 3 9)))
 (assert (member a39 x))
 (declare-fun a310 () (Tuple Int Int))
-(assert (= a310 (mkTuple 3 10)))
+(assert (= a310 (tuple 3 10)))
 (assert (member a310 x))
 (declare-fun a41 () (Tuple Int Int))
-(assert (= a41 (mkTuple 4 1)))
+(assert (= a41 (tuple 4 1)))
 (assert (member a41 x))
 (declare-fun a42 () (Tuple Int Int))
-(assert (= a42 (mkTuple 4 2)))
+(assert (= a42 (tuple 4 2)))
 (assert (member a42 x))
 (declare-fun a43 () (Tuple Int Int))
-(assert (= a43 (mkTuple 4 3)))
+(assert (= a43 (tuple 4 3)))
 (assert (member a43 x))
 (declare-fun a44 () (Tuple Int Int))
-(assert (= a44 (mkTuple 4 4)))
+(assert (= a44 (tuple 4 4)))
 (assert (member a44 x))
 (declare-fun a45 () (Tuple Int Int))
-(assert (= a45 (mkTuple 4 5)))
+(assert (= a45 (tuple 4 5)))
 (assert (member a45 x))
 (declare-fun a46 () (Tuple Int Int))
-(assert (= a46 (mkTuple 4 6)))
+(assert (= a46 (tuple 4 6)))
 (assert (member a46 x))
 (declare-fun a47 () (Tuple Int Int))
-(assert (= a47 (mkTuple 4 7)))
+(assert (= a47 (tuple 4 7)))
 (assert (member a47 x))
 (declare-fun a48 () (Tuple Int Int))
-(assert (= a48 (mkTuple 4 8)))
+(assert (= a48 (tuple 4 8)))
 (assert (member a48 x))
 (declare-fun a49 () (Tuple Int Int))
-(assert (= a49 (mkTuple 4 9)))
+(assert (= a49 (tuple 4 9)))
 (assert (member a49 x))
 (declare-fun a410 () (Tuple Int Int))
-(assert (= a410 (mkTuple 4 10)))
+(assert (= a410 (tuple 4 10)))
 (assert (member a410 x))
 (declare-fun a51 () (Tuple Int Int))
-(assert (= a51 (mkTuple 5 1)))
+(assert (= a51 (tuple 5 1)))
 (assert (member a51 x))
 (declare-fun a52 () (Tuple Int Int))
-(assert (= a52 (mkTuple 5 2)))
+(assert (= a52 (tuple 5 2)))
 (assert (member a52 x))
 (declare-fun a53 () (Tuple Int Int))
-(assert (= a53 (mkTuple 5 3)))
+(assert (= a53 (tuple 5 3)))
 (assert (member a53 x))
 (declare-fun a54 () (Tuple Int Int))
-(assert (= a54 (mkTuple 5 4)))
+(assert (= a54 (tuple 5 4)))
 (assert (member a54 x))
 (declare-fun a55 () (Tuple Int Int))
-(assert (= a55 (mkTuple 5 5)))
+(assert (= a55 (tuple 5 5)))
 (assert (member a55 x))
 (declare-fun a56 () (Tuple Int Int))
-(assert (= a56 (mkTuple 5 6)))
+(assert (= a56 (tuple 5 6)))
 (assert (member a56 x))
 (declare-fun a57 () (Tuple Int Int))
-(assert (= a57 (mkTuple 5 7)))
+(assert (= a57 (tuple 5 7)))
 (assert (member a57 x))
 (declare-fun a58 () (Tuple Int Int))
-(assert (= a58 (mkTuple 5 8)))
+(assert (= a58 (tuple 5 8)))
 (assert (member a58 x))
 (declare-fun a59 () (Tuple Int Int))
-(assert (= a59 (mkTuple 5 9)))
+(assert (= a59 (tuple 5 9)))
 (assert (member a59 x))
 (declare-fun a510 () (Tuple Int Int))
-(assert (= a510 (mkTuple 5 10)))
+(assert (= a510 (tuple 5 10)))
 (assert (member a510 x))
 (declare-fun a61 () (Tuple Int Int))
-(assert (= a61 (mkTuple 6 1)))
+(assert (= a61 (tuple 6 1)))
 (assert (member a61 x))
 (declare-fun a62 () (Tuple Int Int))
-(assert (= a62 (mkTuple 6 2)))
+(assert (= a62 (tuple 6 2)))
 (assert (member a62 x))
 (declare-fun a63 () (Tuple Int Int))
-(assert (= a63 (mkTuple 6 3)))
+(assert (= a63 (tuple 6 3)))
 (assert (member a63 x))
 (declare-fun a64 () (Tuple Int Int))
-(assert (= a64 (mkTuple 6 4)))
+(assert (= a64 (tuple 6 4)))
 (assert (member a64 x))
 (declare-fun a65 () (Tuple Int Int))
-(assert (= a65 (mkTuple 6 5)))
+(assert (= a65 (tuple 6 5)))
 (assert (member a65 x))
 (declare-fun a66 () (Tuple Int Int))
-(assert (= a66 (mkTuple 6 6)))
+(assert (= a66 (tuple 6 6)))
 (assert (member a66 x))
 (declare-fun a67 () (Tuple Int Int))
-(assert (= a67 (mkTuple 6 7)))
+(assert (= a67 (tuple 6 7)))
 (assert (member a67 x))
 (declare-fun a68 () (Tuple Int Int))
-(assert (= a68 (mkTuple 6 8)))
+(assert (= a68 (tuple 6 8)))
 (assert (member a68 x))
 (declare-fun a69 () (Tuple Int Int))
-(assert (= a69 (mkTuple 6 9)))
+(assert (= a69 (tuple 6 9)))
 (assert (member a69 x))
 (declare-fun a610 () (Tuple Int Int))
-(assert (= a610 (mkTuple 6 10)))
+(assert (= a610 (tuple 6 10)))
 (assert (member a610 x))
 (declare-fun a71 () (Tuple Int Int))
-(assert (= a71 (mkTuple 7 1)))
+(assert (= a71 (tuple 7 1)))
 (assert (member a71 x))
 (declare-fun a72 () (Tuple Int Int))
-(assert (= a72 (mkTuple 7 2)))
+(assert (= a72 (tuple 7 2)))
 (assert (member a72 x))
 (declare-fun a73 () (Tuple Int Int))
-(assert (= a73 (mkTuple 7 3)))
+(assert (= a73 (tuple 7 3)))
 (assert (member a73 x))
 (declare-fun a74 () (Tuple Int Int))
-(assert (= a74 (mkTuple 7 4)))
+(assert (= a74 (tuple 7 4)))
 (assert (member a74 x))
 (declare-fun a75 () (Tuple Int Int))
-(assert (= a75 (mkTuple 7 5)))
+(assert (= a75 (tuple 7 5)))
 (assert (member a75 x))
 (declare-fun a76 () (Tuple Int Int))
-(assert (= a76 (mkTuple 7 6)))
+(assert (= a76 (tuple 7 6)))
 (assert (member a76 x))
 (declare-fun a77 () (Tuple Int Int))
-(assert (= a77 (mkTuple 7 7)))
+(assert (= a77 (tuple 7 7)))
 (assert (member a77 x))
 (declare-fun a78 () (Tuple Int Int))
-(assert (= a78 (mkTuple 7 8)))
+(assert (= a78 (tuple 7 8)))
 (assert (member a78 x))
 (declare-fun a79 () (Tuple Int Int))
-(assert (= a79 (mkTuple 7 9)))
+(assert (= a79 (tuple 7 9)))
 (assert (member a79 x))
 (declare-fun a710 () (Tuple Int Int))
-(assert (= a710 (mkTuple 7 10)))
+(assert (= a710 (tuple 7 10)))
 (assert (member a710 x))
 (declare-fun a81 () (Tuple Int Int))
-(assert (= a81 (mkTuple 8 1)))
+(assert (= a81 (tuple 8 1)))
 (assert (member a81 x))
 (declare-fun a82 () (Tuple Int Int))
-(assert (= a82 (mkTuple 8 2)))
+(assert (= a82 (tuple 8 2)))
 (assert (member a82 x))
 (declare-fun a83 () (Tuple Int Int))
-(assert (= a83 (mkTuple 8 3)))
+(assert (= a83 (tuple 8 3)))
 (assert (member a83 x))
 (declare-fun a84 () (Tuple Int Int))
-(assert (= a84 (mkTuple 8 4)))
+(assert (= a84 (tuple 8 4)))
 (assert (member a84 x))
 (declare-fun a85 () (Tuple Int Int))
-(assert (= a85 (mkTuple 8 5)))
+(assert (= a85 (tuple 8 5)))
 (assert (member a85 x))
 (declare-fun a86 () (Tuple Int Int))
-(assert (= a86 (mkTuple 8 6)))
+(assert (= a86 (tuple 8 6)))
 (assert (member a86 x))
 (declare-fun a87 () (Tuple Int Int))
-(assert (= a87 (mkTuple 8 7)))
+(assert (= a87 (tuple 8 7)))
 (assert (member a87 x))
 (declare-fun a88 () (Tuple Int Int))
-(assert (= a88 (mkTuple 8 8)))
+(assert (= a88 (tuple 8 8)))
 (assert (member a88 x))
 (declare-fun a89 () (Tuple Int Int))
-(assert (= a89 (mkTuple 8 9)))
+(assert (= a89 (tuple 8 9)))
 (assert (member a89 x))
 (declare-fun a810 () (Tuple Int Int))
-(assert (= a810 (mkTuple 8 10)))
+(assert (= a810 (tuple 8 10)))
 (assert (member a810 x))
 (declare-fun a91 () (Tuple Int Int))
-(assert (= a91 (mkTuple 9 1)))
+(assert (= a91 (tuple 9 1)))
 (assert (member a91 x))
 (declare-fun a92 () (Tuple Int Int))
-(assert (= a92 (mkTuple 9 2)))
+(assert (= a92 (tuple 9 2)))
 (assert (member a92 x))
 (declare-fun a93 () (Tuple Int Int))
-(assert (= a93 (mkTuple 9 3)))
+(assert (= a93 (tuple 9 3)))
 (assert (member a93 x))
 (declare-fun a94 () (Tuple Int Int))
-(assert (= a94 (mkTuple 9 4)))
+(assert (= a94 (tuple 9 4)))
 (assert (member a94 x))
 (declare-fun a95 () (Tuple Int Int))
-(assert (= a95 (mkTuple 9 5)))
+(assert (= a95 (tuple 9 5)))
 (assert (member a95 x))
 (declare-fun a96 () (Tuple Int Int))
-(assert (= a96 (mkTuple 9 6)))
+(assert (= a96 (tuple 9 6)))
 (assert (member a96 x))
 (declare-fun a97 () (Tuple Int Int))
-(assert (= a97 (mkTuple 9 7)))
+(assert (= a97 (tuple 9 7)))
 (assert (member a97 x))
 (declare-fun a98 () (Tuple Int Int))
-(assert (= a98 (mkTuple 9 8)))
+(assert (= a98 (tuple 9 8)))
 (assert (member a98 x))
 (declare-fun a99 () (Tuple Int Int))
-(assert (= a99 (mkTuple 9 9)))
+(assert (= a99 (tuple 9 9)))
 (assert (member a99 x))
 (declare-fun a910 () (Tuple Int Int))
-(assert (= a910 (mkTuple 9 10)))
+(assert (= a910 (tuple 9 10)))
 (assert (member a910 x))
 (declare-fun a101 () (Tuple Int Int))
-(assert (= a101 (mkTuple 10 1)))
+(assert (= a101 (tuple 10 1)))
 (assert (member a101 x))
 (declare-fun a102 () (Tuple Int Int))
-(assert (= a102 (mkTuple 10 2)))
+(assert (= a102 (tuple 10 2)))
 (assert (member a102 x))
 (declare-fun a103 () (Tuple Int Int))
-(assert (= a103 (mkTuple 10 3)))
+(assert (= a103 (tuple 10 3)))
 (assert (member a103 x))
 (declare-fun a104 () (Tuple Int Int))
-(assert (= a104 (mkTuple 10 4)))
+(assert (= a104 (tuple 10 4)))
 (assert (member a104 x))
 (declare-fun a105 () (Tuple Int Int))
-(assert (= a105 (mkTuple 10 5)))
+(assert (= a105 (tuple 10 5)))
 (assert (member a105 x))
 (declare-fun a106 () (Tuple Int Int))
-(assert (= a106 (mkTuple 10 6)))
+(assert (= a106 (tuple 10 6)))
 (assert (member a106 x))
 (declare-fun a107 () (Tuple Int Int))
-(assert (= a107 (mkTuple 10 7)))
+(assert (= a107 (tuple 10 7)))
 (assert (member a107 x))
 (declare-fun a108 () (Tuple Int Int))
-(assert (= a108 (mkTuple 10 8)))
+(assert (= a108 (tuple 10 8)))
 (assert (member a108 x))
 (declare-fun a109 () (Tuple Int Int))
-(assert (= a109 (mkTuple 10 9)))
+(assert (= a109 (tuple 10 9)))
 (assert (member a109 x))
 (declare-fun a1010 () (Tuple Int Int))
-(assert (= a1010 (mkTuple 10 10)))
+(assert (= a1010 (tuple 10 10)))
 (assert (member a1010 x))
 (declare-fun b11 () (Tuple Int Int))
-(assert (= b11 (mkTuple 1 1)))
+(assert (= b11 (tuple 1 1)))
 (assert (member b11 y))
 (declare-fun b12 () (Tuple Int Int))
-(assert (= b12 (mkTuple 1 2)))
+(assert (= b12 (tuple 1 2)))
 (assert (member b12 y))
 (declare-fun b13 () (Tuple Int Int))
-(assert (= b13 (mkTuple 1 3)))
+(assert (= b13 (tuple 1 3)))
 (assert (member b13 y))
 (declare-fun b14 () (Tuple Int Int))
-(assert (= b14 (mkTuple 1 4)))
+(assert (= b14 (tuple 1 4)))
 (assert (member b14 y))
 (declare-fun b15 () (Tuple Int Int))
-(assert (= b15 (mkTuple 1 5)))
+(assert (= b15 (tuple 1 5)))
 (assert (member b15 y))
 (declare-fun b16 () (Tuple Int Int))
-(assert (= b16 (mkTuple 1 6)))
+(assert (= b16 (tuple 1 6)))
 (assert (member b16 y))
 (declare-fun b17 () (Tuple Int Int))
-(assert (= b17 (mkTuple 1 7)))
+(assert (= b17 (tuple 1 7)))
 (assert (member b17 y))
 (declare-fun b18 () (Tuple Int Int))
-(assert (= b18 (mkTuple 1 8)))
+(assert (= b18 (tuple 1 8)))
 (assert (member b18 y))
 (declare-fun b19 () (Tuple Int Int))
-(assert (= b19 (mkTuple 1 9)))
+(assert (= b19 (tuple 1 9)))
 (assert (member b19 y))
 (declare-fun b110 () (Tuple Int Int))
-(assert (= b110 (mkTuple 1 10)))
+(assert (= b110 (tuple 1 10)))
 (assert (member b110 y))
 (declare-fun b21 () (Tuple Int Int))
-(assert (= b21 (mkTuple 2 1)))
+(assert (= b21 (tuple 2 1)))
 (assert (member b21 y))
 (declare-fun b22 () (Tuple Int Int))
-(assert (= b22 (mkTuple 2 2)))
+(assert (= b22 (tuple 2 2)))
 (assert (member b22 y))
 (declare-fun b23 () (Tuple Int Int))
-(assert (= b23 (mkTuple 2 3)))
+(assert (= b23 (tuple 2 3)))
 (assert (member b23 y))
 (declare-fun b24 () (Tuple Int Int))
-(assert (= b24 (mkTuple 2 4)))
+(assert (= b24 (tuple 2 4)))
 (assert (member b24 y))
 (declare-fun b25 () (Tuple Int Int))
-(assert (= b25 (mkTuple 2 5)))
+(assert (= b25 (tuple 2 5)))
 (assert (member b25 y))
 (declare-fun b26 () (Tuple Int Int))
-(assert (= b26 (mkTuple 2 6)))
+(assert (= b26 (tuple 2 6)))
 (assert (member b26 y))
 (declare-fun b27 () (Tuple Int Int))
-(assert (= b27 (mkTuple 2 7)))
+(assert (= b27 (tuple 2 7)))
 (assert (member b27 y))
 (declare-fun b28 () (Tuple Int Int))
-(assert (= b28 (mkTuple 2 8)))
+(assert (= b28 (tuple 2 8)))
 (assert (member b28 y))
 (declare-fun b29 () (Tuple Int Int))
-(assert (= b29 (mkTuple 2 9)))
+(assert (= b29 (tuple 2 9)))
 (assert (member b29 y))
 (declare-fun b210 () (Tuple Int Int))
-(assert (= b210 (mkTuple 2 10)))
+(assert (= b210 (tuple 2 10)))
 (assert (member b210 y))
 (declare-fun b31 () (Tuple Int Int))
-(assert (= b31 (mkTuple 3 1)))
+(assert (= b31 (tuple 3 1)))
 (assert (member b31 y))
 (declare-fun b32 () (Tuple Int Int))
-(assert (= b32 (mkTuple 3 2)))
+(assert (= b32 (tuple 3 2)))
 (assert (member b32 y))
 (declare-fun b33 () (Tuple Int Int))
-(assert (= b33 (mkTuple 3 3)))
+(assert (= b33 (tuple 3 3)))
 (assert (member b33 y))
 (declare-fun b34 () (Tuple Int Int))
-(assert (= b34 (mkTuple 3 4)))
+(assert (= b34 (tuple 3 4)))
 (assert (member b34 y))
 (declare-fun b35 () (Tuple Int Int))
-(assert (= b35 (mkTuple 3 5)))
+(assert (= b35 (tuple 3 5)))
 (assert (member b35 y))
 (declare-fun b36 () (Tuple Int Int))
-(assert (= b36 (mkTuple 3 6)))
+(assert (= b36 (tuple 3 6)))
 (assert (member b36 y))
 (declare-fun b37 () (Tuple Int Int))
-(assert (= b37 (mkTuple 3 7)))
+(assert (= b37 (tuple 3 7)))
 (assert (member b37 y))
 (declare-fun b38 () (Tuple Int Int))
-(assert (= b38 (mkTuple 3 8)))
+(assert (= b38 (tuple 3 8)))
 (assert (member b38 y))
 (declare-fun b39 () (Tuple Int Int))
-(assert (= b39 (mkTuple 3 9)))
+(assert (= b39 (tuple 3 9)))
 (assert (member b39 y))
 (declare-fun b310 () (Tuple Int Int))
-(assert (= b310 (mkTuple 3 10)))
+(assert (= b310 (tuple 3 10)))
 (assert (member b310 y))
 (declare-fun b41 () (Tuple Int Int))
-(assert (= b41 (mkTuple 4 1)))
+(assert (= b41 (tuple 4 1)))
 (assert (member b41 y))
 (declare-fun b42 () (Tuple Int Int))
-(assert (= b42 (mkTuple 4 2)))
+(assert (= b42 (tuple 4 2)))
 (assert (member b42 y))
 (declare-fun b43 () (Tuple Int Int))
-(assert (= b43 (mkTuple 4 3)))
+(assert (= b43 (tuple 4 3)))
 (assert (member b43 y))
 (declare-fun b44 () (Tuple Int Int))
-(assert (= b44 (mkTuple 4 4)))
+(assert (= b44 (tuple 4 4)))
 (assert (member b44 y))
 (declare-fun b45 () (Tuple Int Int))
-(assert (= b45 (mkTuple 4 5)))
+(assert (= b45 (tuple 4 5)))
 (assert (member b45 y))
 (declare-fun b46 () (Tuple Int Int))
-(assert (= b46 (mkTuple 4 6)))
+(assert (= b46 (tuple 4 6)))
 (assert (member b46 y))
 (declare-fun b47 () (Tuple Int Int))
-(assert (= b47 (mkTuple 4 7)))
+(assert (= b47 (tuple 4 7)))
 (assert (member b47 y))
 (declare-fun b48 () (Tuple Int Int))
-(assert (= b48 (mkTuple 4 8)))
+(assert (= b48 (tuple 4 8)))
 (assert (member b48 y))
 (declare-fun b49 () (Tuple Int Int))
-(assert (= b49 (mkTuple 4 9)))
+(assert (= b49 (tuple 4 9)))
 (assert (member b49 y))
 (declare-fun b410 () (Tuple Int Int))
-(assert (= b410 (mkTuple 4 10)))
+(assert (= b410 (tuple 4 10)))
 (assert (member b410 y))
 (declare-fun b51 () (Tuple Int Int))
-(assert (= b51 (mkTuple 5 1)))
+(assert (= b51 (tuple 5 1)))
 (assert (member b51 y))
 (declare-fun b52 () (Tuple Int Int))
-(assert (= b52 (mkTuple 5 2)))
+(assert (= b52 (tuple 5 2)))
 (assert (member b52 y))
 (declare-fun b53 () (Tuple Int Int))
-(assert (= b53 (mkTuple 5 3)))
+(assert (= b53 (tuple 5 3)))
 (assert (member b53 y))
 (declare-fun b54 () (Tuple Int Int))
-(assert (= b54 (mkTuple 5 4)))
+(assert (= b54 (tuple 5 4)))
 (assert (member b54 y))
 (declare-fun b55 () (Tuple Int Int))
-(assert (= b55 (mkTuple 5 5)))
+(assert (= b55 (tuple 5 5)))
 (assert (member b55 y))
 (declare-fun b56 () (Tuple Int Int))
-(assert (= b56 (mkTuple 5 6)))
+(assert (= b56 (tuple 5 6)))
 (assert (member b56 y))
 (declare-fun b57 () (Tuple Int Int))
-(assert (= b57 (mkTuple 5 7)))
+(assert (= b57 (tuple 5 7)))
 (assert (member b57 y))
 (declare-fun b58 () (Tuple Int Int))
-(assert (= b58 (mkTuple 5 8)))
+(assert (= b58 (tuple 5 8)))
 (assert (member b58 y))
 (declare-fun b59 () (Tuple Int Int))
-(assert (= b59 (mkTuple 5 9)))
+(assert (= b59 (tuple 5 9)))
 (assert (member b59 y))
 (declare-fun b510 () (Tuple Int Int))
-(assert (= b510 (mkTuple 5 10)))
+(assert (= b510 (tuple 5 10)))
 (assert (member b510 y))
 (declare-fun b61 () (Tuple Int Int))
-(assert (= b61 (mkTuple 6 1)))
+(assert (= b61 (tuple 6 1)))
 (assert (member b61 y))
 (declare-fun b62 () (Tuple Int Int))
-(assert (= b62 (mkTuple 6 2)))
+(assert (= b62 (tuple 6 2)))
 (assert (member b62 y))
 (declare-fun b63 () (Tuple Int Int))
-(assert (= b63 (mkTuple 6 3)))
+(assert (= b63 (tuple 6 3)))
 (assert (member b63 y))
 (declare-fun b64 () (Tuple Int Int))
-(assert (= b64 (mkTuple 6 4)))
+(assert (= b64 (tuple 6 4)))
 (assert (member b64 y))
 (declare-fun b65 () (Tuple Int Int))
-(assert (= b65 (mkTuple 6 5)))
+(assert (= b65 (tuple 6 5)))
 (assert (member b65 y))
 (declare-fun b66 () (Tuple Int Int))
-(assert (= b66 (mkTuple 6 6)))
+(assert (= b66 (tuple 6 6)))
 (assert (member b66 y))
 (declare-fun b67 () (Tuple Int Int))
-(assert (= b67 (mkTuple 6 7)))
+(assert (= b67 (tuple 6 7)))
 (assert (member b67 y))
 (declare-fun b68 () (Tuple Int Int))
-(assert (= b68 (mkTuple 6 8)))
+(assert (= b68 (tuple 6 8)))
 (assert (member b68 y))
 (declare-fun b69 () (Tuple Int Int))
-(assert (= b69 (mkTuple 6 9)))
+(assert (= b69 (tuple 6 9)))
 (assert (member b69 y))
 (declare-fun b610 () (Tuple Int Int))
-(assert (= b610 (mkTuple 6 10)))
+(assert (= b610 (tuple 6 10)))
 (assert (member b610 y))
 (declare-fun b71 () (Tuple Int Int))
-(assert (= b71 (mkTuple 7 1)))
+(assert (= b71 (tuple 7 1)))
 (assert (member b71 y))
 (declare-fun b72 () (Tuple Int Int))
-(assert (= b72 (mkTuple 7 2)))
+(assert (= b72 (tuple 7 2)))
 (assert (member b72 y))
 (declare-fun b73 () (Tuple Int Int))
-(assert (= b73 (mkTuple 7 3)))
+(assert (= b73 (tuple 7 3)))
 (assert (member b73 y))
 (declare-fun b74 () (Tuple Int Int))
-(assert (= b74 (mkTuple 7 4)))
+(assert (= b74 (tuple 7 4)))
 (assert (member b74 y))
 (declare-fun b75 () (Tuple Int Int))
-(assert (= b75 (mkTuple 7 5)))
+(assert (= b75 (tuple 7 5)))
 (assert (member b75 y))
 (declare-fun b76 () (Tuple Int Int))
-(assert (= b76 (mkTuple 7 6)))
+(assert (= b76 (tuple 7 6)))
 (assert (member b76 y))
 (declare-fun b77 () (Tuple Int Int))
-(assert (= b77 (mkTuple 7 7)))
+(assert (= b77 (tuple 7 7)))
 (assert (member b77 y))
 (declare-fun b78 () (Tuple Int Int))
-(assert (= b78 (mkTuple 7 8)))
+(assert (= b78 (tuple 7 8)))
 (assert (member b78 y))
 (declare-fun b79 () (Tuple Int Int))
-(assert (= b79 (mkTuple 7 9)))
+(assert (= b79 (tuple 7 9)))
 (assert (member b79 y))
 (declare-fun b710 () (Tuple Int Int))
-(assert (= b710 (mkTuple 7 10)))
+(assert (= b710 (tuple 7 10)))
 (assert (member b710 y))
 (declare-fun b81 () (Tuple Int Int))
-(assert (= b81 (mkTuple 8 1)))
+(assert (= b81 (tuple 8 1)))
 (assert (member b81 y))
 (declare-fun b82 () (Tuple Int Int))
-(assert (= b82 (mkTuple 8 2)))
+(assert (= b82 (tuple 8 2)))
 (assert (member b82 y))
 (declare-fun b83 () (Tuple Int Int))
-(assert (= b83 (mkTuple 8 3)))
+(assert (= b83 (tuple 8 3)))
 (assert (member b83 y))
 (declare-fun b84 () (Tuple Int Int))
-(assert (= b84 (mkTuple 8 4)))
+(assert (= b84 (tuple 8 4)))
 (assert (member b84 y))
 (declare-fun b85 () (Tuple Int Int))
-(assert (= b85 (mkTuple 8 5)))
+(assert (= b85 (tuple 8 5)))
 (assert (member b85 y))
 (declare-fun b86 () (Tuple Int Int))
-(assert (= b86 (mkTuple 8 6)))
+(assert (= b86 (tuple 8 6)))
 (assert (member b86 y))
 (declare-fun b87 () (Tuple Int Int))
-(assert (= b87 (mkTuple 8 7)))
+(assert (= b87 (tuple 8 7)))
 (assert (member b87 y))
 (declare-fun b88 () (Tuple Int Int))
-(assert (= b88 (mkTuple 8 8)))
+(assert (= b88 (tuple 8 8)))
 (assert (member b88 y))
 (declare-fun b89 () (Tuple Int Int))
-(assert (= b89 (mkTuple 8 9)))
+(assert (= b89 (tuple 8 9)))
 (assert (member b89 y))
 (declare-fun b810 () (Tuple Int Int))
-(assert (= b810 (mkTuple 8 10)))
+(assert (= b810 (tuple 8 10)))
 (assert (member b810 y))
 (declare-fun b91 () (Tuple Int Int))
-(assert (= b91 (mkTuple 9 1)))
+(assert (= b91 (tuple 9 1)))
 (assert (member b91 y))
 (declare-fun b92 () (Tuple Int Int))
-(assert (= b92 (mkTuple 9 2)))
+(assert (= b92 (tuple 9 2)))
 (assert (member b92 y))
 (declare-fun b93 () (Tuple Int Int))
-(assert (= b93 (mkTuple 9 3)))
+(assert (= b93 (tuple 9 3)))
 (assert (member b93 y))
 (declare-fun b94 () (Tuple Int Int))
-(assert (= b94 (mkTuple 9 4)))
+(assert (= b94 (tuple 9 4)))
 (assert (member b94 y))
 (declare-fun b95 () (Tuple Int Int))
-(assert (= b95 (mkTuple 9 5)))
+(assert (= b95 (tuple 9 5)))
 (assert (member b95 y))
 (declare-fun b96 () (Tuple Int Int))
-(assert (= b96 (mkTuple 9 6)))
+(assert (= b96 (tuple 9 6)))
 (assert (member b96 y))
 (declare-fun b97 () (Tuple Int Int))
-(assert (= b97 (mkTuple 9 7)))
+(assert (= b97 (tuple 9 7)))
 (assert (member b97 y))
 (declare-fun b98 () (Tuple Int Int))
-(assert (= b98 (mkTuple 9 8)))
+(assert (= b98 (tuple 9 8)))
 (assert (member b98 y))
 (declare-fun b99 () (Tuple Int Int))
-(assert (= b99 (mkTuple 9 9)))
+(assert (= b99 (tuple 9 9)))
 (assert (member b99 y))
 (declare-fun b910 () (Tuple Int Int))
-(assert (= b910 (mkTuple 9 10)))
+(assert (= b910 (tuple 9 10)))
 (assert (member b910 y))
 (declare-fun b101 () (Tuple Int Int))
-(assert (= b101 (mkTuple 10 1)))
+(assert (= b101 (tuple 10 1)))
 (assert (member b101 y))
 (declare-fun b102 () (Tuple Int Int))
-(assert (= b102 (mkTuple 10 2)))
+(assert (= b102 (tuple 10 2)))
 (assert (member b102 y))
 (declare-fun b103 () (Tuple Int Int))
-(assert (= b103 (mkTuple 10 3)))
+(assert (= b103 (tuple 10 3)))
 (assert (member b103 y))
 (declare-fun b104 () (Tuple Int Int))
-(assert (= b104 (mkTuple 10 4)))
+(assert (= b104 (tuple 10 4)))
 (assert (member b104 y))
 (declare-fun b105 () (Tuple Int Int))
-(assert (= b105 (mkTuple 10 5)))
+(assert (= b105 (tuple 10 5)))
 (assert (member b105 y))
 (declare-fun b106 () (Tuple Int Int))
-(assert (= b106 (mkTuple 10 6)))
+(assert (= b106 (tuple 10 6)))
 (assert (member b106 y))
 (declare-fun b107 () (Tuple Int Int))
-(assert (= b107 (mkTuple 10 7)))
+(assert (= b107 (tuple 10 7)))
 (assert (member b107 y))
 (declare-fun b108 () (Tuple Int Int))
-(assert (= b108 (mkTuple 10 8)))
+(assert (= b108 (tuple 10 8)))
 (assert (member b108 y))
 (declare-fun b109 () (Tuple Int Int))
-(assert (= b109 (mkTuple 10 9)))
+(assert (= b109 (tuple 10 9)))
 (assert (member b109 y))
 (declare-fun b1010 () (Tuple Int Int))
-(assert (= b1010 (mkTuple 10 10)))
+(assert (= b1010 (tuple 10 10)))
 (assert (member b1010 y))
-(assert (member (mkTuple 1 9) z))
+(assert (member (tuple 1 9) z))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 9 1)))
+(assert (= a (tuple 9 1)))
 (assert (= r (join (join (transpose x) y) z)))
 (assert (not (member a (transpose r))))
 (check-sat)
diff --git a/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2
index 32d670b25..af871781e 100644
--- a/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2
+++ b/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2
@@ -10,9 +10,9 @@
 (declare-fun d () Int)
 (assert (= a c))
 (assert (= a d))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 2 d) x))
-(assert (member (mkTuple a 5) y))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 2 d) x))
+(assert (member (tuple a 5) y))
 (assert (= y (tclosure x)))
-(assert (member (mkTuple 2 5) y))
+(assert (member (tuple 2 5) y))
 (check-sat)
diff --git a/test/regress/regress1/rels/rel_tc_4.cvc.smt2 b/test/regress/regress1/rels/rel_tc_4.cvc.smt2
index 29cb0609f..5de402d3b 100644
--- a/test/regress/regress1/rels/rel_tc_4.cvc.smt2
+++ b/test/regress/regress1/rels/rel_tc_4.cvc.smt2
@@ -8,11 +8,11 @@
 (declare-fun b () Int)
 (declare-fun c () Int)
 (declare-fun d () Int)
-(assert (member (mkTuple 1 a) x))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 1 d) x))
-(assert (member (mkTuple b 1) x))
+(assert (member (tuple 1 a) x))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 1 d) x))
+(assert (member (tuple b 1) x))
 (assert (= b d))
-(assert (member (mkTuple 2 b) (join (join x x) x)))
-(assert (not (member (mkTuple 2 1) (tclosure x))))
+(assert (member (tuple 2 b) (join (join x x) x)))
+(assert (not (member (tuple 2 1) (tclosure x))))
 (check-sat)
diff --git a/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2
index 599d30946..0cfacd14a 100644
--- a/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2
+++ b/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2
@@ -8,15 +8,15 @@
 (declare-fun w () (Set (Tuple Int Int)))
 (assert (= z (tclosure x)))
 (assert (= w (join x y)))
-(assert (member (mkTuple 2 2) z))
-(assert (member (mkTuple 0 3) y))
-(assert (member (mkTuple (- 1) 3) y))
-(assert (member (mkTuple 1 3) y))
-(assert (member (mkTuple (- 2) 3) y))
-(assert (member (mkTuple 2 3) y))
-(assert (member (mkTuple 3 3) y))
-(assert (member (mkTuple 4 3) y))
-(assert (member (mkTuple 5 3) y))
-(assert (not (member (mkTuple 2 3) (join x y))))
-(assert (not (member (mkTuple 2 1) x)))
+(assert (member (tuple 2 2) z))
+(assert (member (tuple 0 3) y))
+(assert (member (tuple (- 1) 3) y))
+(assert (member (tuple 1 3) y))
+(assert (member (tuple (- 2) 3) y))
+(assert (member (tuple 2 3) y))
+(assert (member (tuple 3 3) y))
+(assert (member (tuple 4 3) y))
+(assert (member (tuple 5 3) y))
+(assert (not (member (tuple 2 3) (join x y))))
+(assert (not (member (tuple 2 1) x)))
 (check-sat)
diff --git a/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 b/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2
index 1a71721ac..698d29081 100644
--- a/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2
+++ b/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2
@@ -6,13 +6,13 @@
 (declare-fun y () (Set (Tuple Int Int)))
 (declare-fun z () (Set (Tuple Int Int)))
 (declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
 (declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
 (assert (= r (join (join (transpose x) y) z)))
 (assert (member a (transpose r)))
 (check-sat)
diff --git a/test/regress/regress1/rels/set-strat.cvc.smt2 b/test/regress/regress1/rels/set-strat.cvc.smt2
index e1c82de24..53e5588a9 100644
--- a/test/regress/regress1/rels/set-strat.cvc.smt2
+++ b/test/regress/regress1/rels/set-strat.cvc.smt2
@@ -13,8 +13,8 @@
 (assert (member a x))
 (assert (member b y))
 (assert (member b w))
-(assert (member (mkTuple x y) z))
-(assert (member (mkTuple w x) z))
-(assert (not (member (mkTuple x x) (join z z))))
-(assert (member (mkTuple x (singleton (mkTuple 0 0))) (join z z)))
+(assert (member (tuple x y) z))
+(assert (member (tuple w x) z))
+(assert (not (member (tuple x x) (join z z))))
+(assert (member (tuple x (singleton (tuple 0 0))) (join z z)))
 (check-sat)
diff --git a/test/regress/regress1/rels/strat.cvc.smt2 b/test/regress/regress1/rels/strat.cvc.smt2
index 0cc6905f2..42850d283 100644
--- a/test/regress/regress1/rels/strat.cvc.smt2
+++ b/test/regress/regress1/rels/strat.cvc.smt2
@@ -13,8 +13,8 @@
 (assert (not (= a b)))
 (assert (member a z))
 (assert (member b z))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple b a) x))
+(assert (member (tuple a b) x))
+(assert (member (tuple b a) x))
 (assert (member c x))
-(assert (and (not (= c (mkTuple a b))) (not (= c (mkTuple b a)))))
+(assert (and (not (= c (tuple a b))) (not (= c (tuple b a)))))
 (check-sat)
diff --git a/test/regress/regress1/sets/issue4124-need-check.smt2 b/test/regress/regress1/sets/issue4124-need-check.smt2
index 3ad43ea98..46507df2a 100644
--- a/test/regress/regress1/sets/issue4124-need-check.smt2
+++ b/test/regress/regress1/sets/issue4124-need-check.smt2
@@ -6,8 +6,8 @@
 (declare-fun d () (Set (Tuple String String))) 
 (declare-fun f () (Set Int)) 
 (declare-fun e () Int) 
-(assert (= b (insert (mkTuple "" 1)  (mkTuple "" 2) (singleton (mkTuple "" 4))))) 
-(assert (= c (insert (mkTuple 1 "1") (mkTuple 2 "2") (singleton (mkTuple 7 ""))))) 
+(assert (= b (insert (tuple "" 1)  (tuple "" 2) (singleton (tuple "" 4))))) 
+(assert (= c (insert (tuple 1 "1") (tuple 2 "2") (singleton (tuple 7 ""))))) 
 (assert (= d (join b c)))    
 (assert (= e (card f))) 
 (check-sat)
diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2
index d15aa3030..d75b9c3ae 100644
--- a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2
+++ b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2
@@ -6,8 +6,8 @@
 (declare-fun a () (Set (Tuple Real Int)))
 (declare-fun b () (Set (Tuple Int Real)))
 (declare-fun x () (Tuple Real Real))
-(assert (let ((_let_1 0.0)) (not (= x (mkTuple _let_1 _let_1)))))
-(assert (member (mkTuple ((_ tupSel 0) x) (to_int ((_ tupSel 1) x))) a))
-(assert (member (mkTuple (to_int ((_ tupSel 0) x)) ((_ tupSel 1) x)) b))
-(assert (not (= ((_ tupSel 0) x) ((_ tupSel 1) x))))
+(assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1)))))
+(assert (member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a))
+(assert (member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b))
+(assert (not (= ((_ tuple_select 0) x) ((_ tuple_select 1) x))))
 (check-sat)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 63556fa8a..19113ae13 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -2520,7 +2520,7 @@ TEST_F(TestApiBlackSolver, tupleProject)
   }
 
   ASSERT_EQ(
-      "((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton "
+      "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (singleton "
       "\"Z\")))",
       projection.toString());
 }