summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rels/bv2.cvc.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rels/bv2.cvc.smt2')
-rw-r--r--test/regress/regress1/rels/bv2.cvc.smt28
1 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress1/rels/bv2.cvc.smt2 b/test/regress/regress1/rels/bv2.cvc.smt2
index 005737b36..9ea472819 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 (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))))
+(assert (set.member (tuple a b) x))
+(assert (set.member (tuple a c) x))
+(assert (set.member (tuple d a) y))
+(assert (not (set.member (tuple a a) (rel.join x y))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback