diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:06:38 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:06:38 +0100 |
| commit | f45eb9f44f32cbab80e0aaaff167f6b60b9abbc3 (patch) | |
| tree | eab9f6d13cac311e81e88f61499d838b33fd7803 /Test/test16/LoopUnroll.bpl.1.expect | |
| parent | 3fe0bfbc9230088a398a0d500092ed9476fe136d (diff) | |
Enabled lit loop unrolling test
Diffstat (limited to 'Test/test16/LoopUnroll.bpl.1.expect')
| -rw-r--r-- | Test/test16/LoopUnroll.bpl.1.expect | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Test/test16/LoopUnroll.bpl.1.expect b/Test/test16/LoopUnroll.bpl.1.expect new file mode 100644 index 00000000..e86e03d7 --- /dev/null +++ b/Test/test16/LoopUnroll.bpl.1.expect @@ -0,0 +1,7 @@ +LoopUnroll.bpl(62,5): Error BP5001: This assertion might not hold. +Execution trace: + LoopUnroll.bpl(58,5): anon0#1 + LoopUnroll.bpl(59,3): anon2_LoopHead#1 + LoopUnroll.bpl(61,5): anon2_LoopBody#1 + +Boogie program verifier finished with 2 verified, 1 error |