main
| Rev | Line | |
|---|
| [c2b37db] | 1 | #include<mem.cvh>
|
|---|
| 2 |
|
|---|
| 3 | $input int N,M;
|
|---|
| 4 | $assume(6 <= N && N <= 10);
|
|---|
| 5 | $assume(N <= M && M <= 2*N);
|
|---|
| 6 | int a[N][M];
|
|---|
| 7 |
|
|---|
| 8 | int main() {
|
|---|
| 9 | $mem m = &a[0 .. N-1][0 .. M-1];
|
|---|
| 10 | $mem m2 = &a[N-5 .. N-2][2 .. M-4];
|
|---|
| 11 | m = $mem_diff(m, m2);
|
|---|
| 12 | $mem m3 = &a[0..N-6][0..M-1];
|
|---|
| 13 | m3 = $mem_union(m3, &a[N-1..N-1][0..M-1]);
|
|---|
| 14 | m3 = $mem_union(m3, &a[0..N-1][0..1]);
|
|---|
| 15 | m3 = $mem_union(m3, &a[0..N-1][M-3..M-1]);
|
|---|
| 16 | $assert($mem_contains(m, m3));
|
|---|
| 17 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
