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/VCGeneration | |
| 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/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 134cff4c..24e083d0 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -49,19 +49,7 @@ namespace Microsoft.Boogie { public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {
- if (impl == null)
- return CommandLineOptions.Clo.Bitvectors;
- bool force_int = false;
- bool force_native = false;
- cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);
- impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
- impl.CheckBooleanAttribute("forceBvInt", ref force_int);
- impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);
- if (force_native)
- return CommandLineOptions.BvHandling.Z3Native;
- if (force_int)
- return CommandLineOptions.BvHandling.ToInt;
- return CommandLineOptions.Clo.Bitvectors;
+ return CommandLineOptions.BvHandling.Z3Native;
}
public bool WillingToHandle(Implementation impl, int timeout) {
|