diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
| commit | ae44269a34b002797b2583b93a0041059b57cbda (patch) | |
| tree | 3ec4a7a8ca3477298f93feb1267d854062a26417 /Source/Core/AbsyExpr.cs | |
| parent | 6be1fd5fa2617602d0a86e95d656018b172ef8d2 (diff) | |
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 5 |
1 files changed, 0 insertions, 5 deletions
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;
|