diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
| commit | ae44269a34b002797b2583b93a0041059b57cbda (patch) | |
| tree | 3ec4a7a8ca3477298f93feb1267d854062a26417 /Test/extractloops | |
| parent | 6be1fd5fa2617602d0a86e95d656018b172ef8d2 (diff) | |
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
Diffstat (limited to 'Test/extractloops')
| -rw-r--r-- | Test/extractloops/Answer | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index 9a6c95a3..954ea799 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -64,6 +64,10 @@ Boogie program verifier finished with 1 verified, 0 errors t3.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
t3.bpl(19,3): anon0
+ t3.bpl(23,3): anon3_LoopHead
+ Inlined call to procedure foo begins
+ t3.bpl(11,5): anon0
+ Inlined call to procedure foo ends
t3.bpl(27,3): anon3_LoopBody
t3.bpl(23,3): anon3_LoopHead
Inlined call to procedure foo begins
|