summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/nonvar-univ.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/nonvar-univ.smt2')
-rw-r--r--test/regress/regress0/sets/nonvar-univ.smt26
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2
index 5c3bc567c..695e87ec3 100644
--- a/test/regress/regress0/sets/nonvar-univ.smt2
+++ b/test/regress/regress0/sets/nonvar-univ.smt2
@@ -6,8 +6,8 @@
(declare-fun P ((Set Int)) Bool)
(assert (P x))
-(assert (not (P (singleton 0))))
-(assert (member 1 x))
-(assert (not (member 0 (as univset (Set Int)))))
+(assert (not (P (set.singleton 0))))
+(assert (set.member 1 x))
+(assert (not (set.member 0 (as set.universe (Set Int)))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback