summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rels/rel_join_4.cvc.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/rels/rel_join_4.cvc.smt2')
-rw-r--r--test/regress/regress0/rels/rel_join_4.cvc.smt220
1 files changed, 10 insertions, 10 deletions
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))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback