From ae44269a34b002797b2583b93a0041059b57cbda Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Oct 2011 14:22:08 -0700 Subject: Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. --- Test/test2/runtest.bat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/test2') diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat index 3dc7d0c3..8ce2f66e 100644 --- a/Test/test2/runtest.bat +++ b/Test/test2/runtest.bat @@ -24,7 +24,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do ( ) echo -------------------- sk_hack.bpl -------------------- -%BGEXE% %* /noinfer /bv:z sk_hack.bpl +%BGEXE% %* /noinfer sk_hack.bpl for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do ( echo. -- cgit v1.2.3