We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 24ae8e1 commit a225a98Copy full SHA for a225a98
Test/extractloops/irreducibleExtract.bpl
@@ -0,0 +1,22 @@
1
+// RUN: %parallel-boogie -extractLoops "%s" > "%t"
2
+// RUN: %OutputCheck --file-to-check "%t" "%s"
3
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
4
+
5
+procedure {:entrypoint} simple_irreducible() {
6
+ var x: int;
7
+ x := 0;
8
+ A:
9
+ assume x == 0;
10
+ x := x + 1;
11
+ goto B, C;
12
13
+ B:
14
+ assume x <= 2;
15
+ x := x - 1;
16
+ goto C, D;
17
+ C:
18
19
+ goto B;
20
+ D:
21
+ assume x <= 1;
22
+}
0 commit comments