We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 28450ac commit 7be7545Copy full SHA for 7be7545
Test/civl/samples/TryIncN.bpl
@@ -18,7 +18,6 @@ refines atomic action {:layer 2} _{
18
return;
19
}
20
21
-
22
// Helper recursive procedure
23
yield procedure {:layer 1} HelperInc(tries: int, limit: int) returns (ok: bool)
24
refines atomic action {:layer 2} _{
@@ -53,8 +52,6 @@ action {:layer 2} AtomicComputeLimit() returns (limit: int) {
53
52
assume limit > 0;
54
55
56
57
58
yield procedure {:layer 0} CAS(prev: int, next: int) returns (ok: bool);
59
refines atomic action {:layer 1} _ {
60
ok := (count == prev);
0 commit comments