summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/univset-simp.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/univset-simp.smt2')
-rw-r--r--test/regress/regress0/sets/univset-simp.smt214
1 files changed, 7 insertions, 7 deletions
diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
index a8875cc41..04f413399 100644
--- a/test/regress/regress0/sets/univset-simp.smt2
+++ b/test/regress/regress0/sets/univset-simp.smt2
@@ -12,12 +12,12 @@
(declare-fun x () Int)
-(assert (not (member 0 a)))
-(assert (member 0 b))
-(assert (not (member 1 c)))
-(assert (member 2 d))
-(assert (= e (as univset (Set Int))))
-(assert (= f (complement d)))
-(assert (not (member x (as univset (Set Int)))))
+(assert (not (set.member 0 a)))
+(assert (set.member 0 b))
+(assert (not (set.member 1 c)))
+(assert (set.member 2 d))
+(assert (= e (as set.universe (Set Int))))
+(assert (= f (set.complement d)))
+(assert (not (set.member x (as set.universe (Set Int)))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback