diff options
| -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
|