source:
CIVL/examples/languageFeatures/forall4.cvl
| Last change on this file was 4f61660, checked in by , 3 months ago | |
|---|---|
|
|
| File size: 176 bytes | |
| Line | |
|---|---|
| 1 | $input int n; |
| 2 | $assume(n>=1); |
| 3 | $input int a[n], b[n]; |
| 4 | int main() { |
| 5 | $assume($forall (int j: 0..n-1) a[j] == 0 && b[j] == a[j]); |
| 6 | $assert($forall (int j: 0..n-1) b[j]==a[j]); |
| 7 | } |
Note:
See TracBrowser
for help on using the repository browser.
