diff options
| author |  MichalMoskal <unknown> | 2010-08-10 16:56:13 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-08-10 16:56:13 +0000 |
| commit | 44ef3e77d948ebec94287665fdfdf57d35fafbf1 (patch) | |
| tree | 39245f90719556b086d556776948b7e76a4dade3 /Test/bitvectors/Answer | |
| parent | 27a5f7a4a7e08ac81c28342565b63ed5e24a8ecd (diff) | |
Fix the test to use new name for /z3bv option.
Diffstat (limited to 'Test/bitvectors/Answer')
| -rw-r--r-- | Test/bitvectors/Answer | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index aa060ee4..0299fff6 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -37,19 +37,19 @@ bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z -------------------- bv5.bpl --------------------
bv5.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
- bv5.bpl(5,12): anon0
+ bv5.bpl(5,12): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- bv6.bpl --------------------
bv6.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
- bv6.bpl(5,5): anon0
+ bv6.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- bv8.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
--------------------- bv9.bpl /bv:z /z3bv --------------------
+-------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
Boogie program verifier finished with 1 verified, 0 errors
|