diff options
Diffstat (limited to 'test/regress/regress1/rels/set-strat.cvc.smt2')
| -rw-r--r-- | test/regress/regress1/rels/set-strat.cvc.smt2 | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/test/regress/regress1/rels/set-strat.cvc.smt2 b/test/regress/regress1/rels/set-strat.cvc.smt2 index 53e5588a9..a509780ac 100644 --- a/test/regress/regress1/rels/set-strat.cvc.smt2 +++ b/test/regress/regress1/rels/set-strat.cvc.smt2 @@ -10,11 +10,11 @@ (declare-fun a () (Tuple Int Int)) (declare-fun b () (Tuple Int Int)) (assert (not (= a b))) -(assert (member a x)) -(assert (member b y)) -(assert (member b w)) -(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))) +(assert (set.member a x)) +(assert (set.member b y)) +(assert (set.member b w)) +(assert (set.member (tuple x y) z)) +(assert (set.member (tuple w x) z)) +(assert (not (set.member (tuple x x) (rel.join z z)))) +(assert (set.member (tuple x (set.singleton (tuple 0 0))) (rel.join z z))) (check-sat) |