diff options
Diffstat (limited to 'Test/prover/z3mutl.bpl')
-rw-r--r-- | Test/prover/z3mutl.bpl | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl new file mode 100644 index 00000000..73cd62b1 --- /dev/null +++ b/Test/prover/z3mutl.bpl @@ -0,0 +1,22 @@ +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 |