summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/CommandLineOptions.cs5
-rw-r--r--Source/Core/VCExp.cs1
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;