From ae44269a34b002797b2583b93a0041059b57cbda Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Oct 2011 14:22:08 -0700 Subject: Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. --- Test/extractloops/Answer | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Test/extractloops') 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 -- cgit v1.2.3