summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-07-09 12:38:12 -0700
committerGravatar qadeer <qadeer@microsoft.com>2011-07-09 12:38:12 -0700
commitb1b84b22d16894e5ea2bc7d677eb83c011cb6964 (patch)
tree6fa7b6c9a35d63798dcb159810fc933bb065e39f /Test
parent574a0863cb34fb612ecf3d107416c955bdf889a8 (diff)
fixed bug in vcgen for bitvectors
Diffstat (limited to 'Test')
-rw-r--r--Test/bitvectors/Answer3
-rw-r--r--Test/bitvectors/runtest.bat2
2 files changed, 4 insertions, 1 deletions
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
index 6f4068c6..f0f65b04 100644
--- a/Test/bitvectors/Answer
+++ b/Test/bitvectors/Answer
@@ -49,6 +49,9 @@ Boogie program verifier finished with 0 verified, 1 error
-------------------- bv8.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
+-------------------- bv10.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
index fd5136f5..a0480645 100644
--- a/Test/bitvectors/runtest.bat
+++ b/Test/bitvectors/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do (
echo -------------------- bv4.bpl - /bv:n --------------------
%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl
-for %%f in (bv5.bpl bv6.bpl bv8.bpl) do (
+for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)