summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/rels/rels-sharing-simp.cvc.smt2')
-rw-r--r--test/regress/regress0/rels/rels-sharing-simp.cvc.smt26
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 b/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2
index 2ba92270a..186374897 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 (tuple 1 x) w))
-(assert (member (tuple y 2) z))
-(assert (not (member (tuple 1 2) (join w z))))
+(assert (set.member (tuple 1 x) w))
+(assert (set.member (tuple y 2) z))
+(assert (not (set.member (tuple 1 2) (rel.join w z))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback