diff options
author | 2011-10-27 14:46:57 -0700 | |
---|---|---|
committer | 2011-10-27 14:46:57 -0700 | |
commit | 7b4af4309de9ae134eac20af13a87f1036733e0d (patch) | |
tree | e4f0a8d8ff3b16153a90620b2dc2b7937e7aac28 /Source/Core | |
parent | ae44269a34b002797b2583b93a0041059b57cbda (diff) |
Boogie: internal clean-up, removed BvHandling type, everything now behaves as if the old /bv:z were used
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 5 | ||||
-rw-r--r-- | Source/Core/VCExp.cs | 1 |
2 files changed, 0 insertions, 6 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 8647e79e..f23f4833 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -236,11 +236,6 @@ namespace Microsoft.Boogie { public string/*?*/ ModelViewFile = null;
public int EnhancedErrorMessages = 0;
public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
- public enum BvHandling {
- None,
- Z3Native,
- ToInt
- }
public bool UseArrayTheory = false;
public bool MonomorphicArrays {
get {
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs index f6a976e5..6bc43e14 100644 --- a/Source/Core/VCExp.cs +++ b/Source/Core/VCExp.cs @@ -29,7 +29,6 @@ namespace Microsoft.Boogie { public bool ForceLogStatus = false;
public int TimeLimit = 0;
public int MemoryLimit = 0;
- public CommandLineOptions.BvHandling BitVectors = CommandLineOptions.BvHandling.None;
public int Verbosity = 0;
public string ProverPath;
|