diff options
Diffstat (limited to 'Test/prover/z3mutl.bpl')
-rw-r--r-- | Test/prover/z3mutl.bpl | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl index f42f7bb4..84b82ed6 100644 --- a/Test/prover/z3mutl.bpl +++ b/Test/prover/z3mutl.bpl @@ -1,24 +1,24 @@ -// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var x:int;
-
-procedure Foo(){
-
-start:
-
- goto L1, L2, L3, L4;
-L1: assume x == 1;
- goto L5;
-
-L2: assume x == 2;
- goto L5;
-
-L3: assume x == 3;
- goto L5;
-
-L4: assume x > 10;
- goto L5;
-
-L5: assert (x > 4);
-
+// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var x:int; + +procedure Foo(){ + +start: + + goto L1, L2, L3, L4; +L1: assume x == 1; + goto L5; + +L2: assume x == 2; + goto L5; + +L3: assume x == 3; + goto L5; + +L4: assume x > 10; + goto L5; + +L5: assert (x > 4); + }
\ No newline at end of file |