summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/cvc-sample.cvc.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/cvc-sample.cvc.smt2')
-rw-r--r--test/regress/regress0/sets/cvc-sample.cvc.smt24
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2
index 9ee199b43..9c89df0c6 100644
--- a/test/regress/regress0/sets/cvc-sample.cvc.smt2
+++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2
@@ -20,12 +20,12 @@
(declare-fun e () Int)
(assert (= a (set.singleton 5)))
(assert (= c (set.union a b)))
-(assert (not (= c (set.intersection a b))))
+(assert (not (= c (set.inter a b))))
(assert (= c (set.minus a b)))
(assert (set.subset a b))
(assert (set.member e c))
(assert (set.member e a))
-(assert (set.member e (set.intersection a b)))
+(assert (set.member e (set.inter a b)))
(push 1)
(assert true)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback