summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2')
-rw-r--r--test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt24
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
index bc2f103d2..55b4ac581 100644
--- a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
+++ b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
@@ -2,7 +2,7 @@
(set-info :status unsat)
(declare-fun st3 () (Set String))
(declare-fun st9 () (Set String))
-(assert (set.is_singleton (set.intersection st3 st9)))
-(assert (< 1 (set.card (set.intersection st3 st9))))
+(assert (set.is_singleton (set.inter st3 st9)))
+(assert (< 1 (set.card (set.inter st3 st9))))
(assert (set.is_singleton st9))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback