source:
CIVL/examples/library/civlc/elaborate.cvl@
0fdf4bd
| Last change on this file since 0fdf4bd was 3ff27cf, checked in by , 11 years ago | |
|---|---|
|
|
| File size: 189 bytes | |
| Rev | Line | |
|---|---|---|
| [6f8bc6ea] | 1 | #include <stdio.h> |
| 2 | #include <civlc.cvh> | |
| 3 | ||
| 4 | $input int X; | |
| [3ff27cf] | 5 | $assume(1 <= X && X <= 3); |
| 6 | $assume(X % 2 == 0); | |
| [6f8bc6ea] | 7 | |
| 8 | int main(void) { | |
| 9 | elaborate(X); | |
| 10 | printf("%d\n", X); | |
| [3ff27cf] | 11 | $assert(X==2); |
| [6f8bc6ea] | 12 | return 0; |
| 13 | } |
Note:
See TracBrowser
for help on using the repository browser.
