diff options
Diffstat (limited to 'test/regress/regress1/sets/card-vc6-minimized.smt2')
| -rw-r--r-- | test/regress/regress1/sets/card-vc6-minimized.smt2 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress1/sets/card-vc6-minimized.smt2 b/test/regress/regress1/sets/card-vc6-minimized.smt2 index d7f4bdf1e..4f589cad7 100644 --- a/test/regress/regress1/sets/card-vc6-minimized.smt2 +++ b/test/regress/regress1/sets/card-vc6-minimized.smt2 @@ -6,10 +6,10 @@ (declare-fun alloc1 () (Set Int)) (declare-fun alloc2 () (Set Int)) (assert -(and (member x c) - (<= (card (setminus alloc1 alloc0)) 1) - (<= (card (setminus alloc2 alloc1)) - (card (setminus c (singleton x)))) - (> (card (setminus alloc2 alloc0)) (card c)) +(and (set.member x c) + (<= (set.card (set.minus alloc1 alloc0)) 1) + (<= (set.card (set.minus alloc2 alloc1)) + (set.card (set.minus c (set.singleton x)))) + (> (set.card (set.minus alloc2 alloc0)) (set.card c)) )) (check-sat) |