diff options
| author |  Shuvendu Lahiri <shuvendu@microsoft.com> | 2015-10-27 17:40:33 -0700 |
|---|---|---|
| committer | Shuvendu Lahiri <shuvendu@microsoft.com> | 2015-10-27 17:40:33 -0700 |
| commit | 02f5c060ca5ce6bff003034ed634c114d5592398 (patch) | |
| tree | 272d491b09fc5606928de9325803b4345843c5d3 /Test/extractloops/detLoopExtractNested.bpl.expect | |
| parent | e037ca99cdc163ca43690aaef3c380ebc1ce1962 (diff) | |
fix for deterministicExtractLoops for nested loops
Diffstat (limited to 'Test/extractloops/detLoopExtractNested.bpl.expect')
| -rw-r--r-- | Test/extractloops/detLoopExtractNested.bpl.expect | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Test/extractloops/detLoopExtractNested.bpl.expect b/Test/extractloops/detLoopExtractNested.bpl.expect new file mode 100644 index 00000000..f4932ede --- /dev/null +++ b/Test/extractloops/detLoopExtractNested.bpl.expect @@ -0,0 +1,19 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + detLoopExtractNested.bpl(12,12): anon0 + detLoopExtractNested.bpl(14,8): anon5_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(14,8): anon5_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(13,4): anon5_LoopDone + detLoopExtractNested.bpl(13,4): anon5_LoopDone + +Boogie program verifier finished with 0 verified, 1 error |