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 | |
| parent | 27a5f7a4a7e08ac81c28342565b63ed5e24a8ecd (diff) | |
Fix the test to use new name for /z3bv option.
| -rw-r--r-- | Test/bitvectors/Answer | 6 | ||||
| -rw-r--r-- | Test/bitvectors/runtest.bat | 4 |
2 files changed, 5 insertions, 5 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
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat index 2ec881fd..0ed64df1 100644 --- a/Test/bitvectors/runtest.bat +++ b/Test/bitvectors/runtest.bat @@ -16,5 +16,5 @@ for %%f in (bv5.bpl bv6.bpl bv8.bpl) do ( %BGEXE% %* %%f
)
-echo -------------------- bv9.bpl /bv:z /z3bv --------------------
-%BGEXE% /bv:z /z3bv bv9.bpl
\ No newline at end of file +echo -------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
+%BGEXE% /bv:z /proverOpt:OPTIMIZE_FOR_BV=true bv9.bpl
|