summaryrefslogtreecommitdiff
path: root/Test/bitvectors/runtest.bat
diff options
context:
space:
mode:
Diffstat (limited to 'Test/bitvectors/runtest.bat')
-rw-r--r--Test/bitvectors/runtest.bat5
1 files changed, 1 insertions, 4 deletions
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
index 0fc17990..cbafa065 100644
--- a/Test/bitvectors/runtest.bat
+++ b/Test/bitvectors/runtest.bat
@@ -3,14 +3,11 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl vcc0.bpl) do (
+for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% /proverWarnings:1 /bv:z %* /logPrefix:-0 %%f
)
-echo -------------------- vcc0.bpl - toInt --------------------
-%BGEXE% /proverWarnings:1 /bv:i /proc:foo %* /logPrefix:-1 vcc0.bpl
-
echo -------------------- bv4.bpl - /bv:n --------------------
%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl