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. --- Source/Core/AbsyExpr.cs | 5 ----- 1 file changed, 5 deletions(-) (limited to 'Source/Core/AbsyExpr.cs') diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 630f6f14..9a0fe64e 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -494,8 +494,6 @@ namespace Microsoft.Boogie { public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); - if (Val is BvConst && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) - tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag"); this.Type = ShallowType; } @@ -2241,9 +2239,6 @@ namespace Microsoft.Boogie { TypeParameters == null) { TypeParamInstantiation tpInsts; Type = Fun.Typecheck(ref Args, out tpInsts, tc); - if (Type != null && Type.IsBv && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) { - tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag"); - } TypeParameters = tpInsts; } IOverloadedAppliable oa = Fun as IOverloadedAppliable; -- cgit v1.2.3