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