Skip to content

Commit cdd9806

Browse files
author
Pramod Subramanyan
committed
Merge branch 'master' of github.com:uclid-org/uclid
2 parents 2160f7c + 1265b3e commit cdd9806

File tree

1 file changed

+24
-0
lines changed

1 file changed

+24
-0
lines changed
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
module main {
2+
// System description.
3+
var a, b : int;
4+
5+
init {
6+
havoc a;
7+
havoc b;
8+
// embedded assumptions.
9+
assume (a <= b);
10+
assume (a >= 0 && b >= 0);
11+
}
12+
next {
13+
a, b = b, a + b;
14+
// embedded assertion.
15+
assert (a <= b);
16+
}
17+
18+
// Proof script.
19+
control {
20+
unroll (3);
21+
check;
22+
print_results;
23+
}
24+
}

0 commit comments

Comments
 (0)