From 7b4af4309de9ae134eac20af13a87f1036733e0d Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 27 Oct 2011 14:46:57 -0700
Subject: Boogie: internal clean-up, removed BvHandling type, everything now
 behaves as if the old /bv:z were used

---
 Source/VCGeneration/Check.cs | 21 +++++----------------
 1 file changed, 5 insertions(+), 16 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 24e083d0..ff691828 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -33,7 +33,6 @@ namespace Microsoft.Boogie {
     private readonly VCExpressionGenerator gen;
 
     private ProverInterface thmProver;
-    private CommandLineOptions.BvHandling bitvectors;
     private int timeout;
 
     // state for the async interface
@@ -48,12 +47,8 @@ namespace Microsoft.Boogie {
 
     public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
 
-    private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {
-      return CommandLineOptions.BvHandling.Z3Native;
-    }
-
     public bool WillingToHandle(Implementation impl, int timeout) {
-      return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);
+      return !closed && timeout == this.timeout;
     }
 
     public VCExpressionGenerator VCExprGen {
@@ -79,13 +74,10 @@ namespace Microsoft.Boogie {
       }
 
       public readonly Program program;
-      public readonly CommandLineOptions.BvHandling bitvectors;
 
-      public ContextCacheKey(Program prog,
-                             CommandLineOptions.BvHandling bitvectors) {
+      public ContextCacheKey(Program prog) {
         Contract.Requires(prog != null);
         this.program = prog;
-        this.bitvectors = bitvectors;
       }
 
       [Pure]
@@ -93,15 +85,14 @@ namespace Microsoft.Boogie {
       public override bool Equals(object that) {
         if (that is ContextCacheKey) {
           ContextCacheKey thatKey = (ContextCacheKey)that;
-          return this.program.Equals(thatKey.program) &&
-                 this.bitvectors.Equals(thatKey.bitvectors);
+          return this.program.Equals(thatKey.program);
         }
         return false;
       }
 
       [Pure]
       public override int GetHashCode() {
-        return this.program.GetHashCode() + this.bitvectors.GetHashCode();
+        return this.program.GetHashCode();
       }
     }
 
@@ -113,7 +104,6 @@ namespace Microsoft.Boogie {
     public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) {
       Contract.Requires(vcgen != null);
       Contract.Requires(prog != null);
-      this.bitvectors = BvHandlingForImpl(impl);
       this.timeout = timeout;
 
       ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
@@ -127,11 +117,10 @@ namespace Microsoft.Boogie {
       if (timeout > 0) {
         options.TimeLimit = timeout * 1000;
       }
-      options.BitVectors = this.bitvectors;
 
       options.Parse(CommandLineOptions.Clo.ProverOptions);
 
-      ContextCacheKey key = new ContextCacheKey(prog, this.bitvectors);
+      ContextCacheKey key = new ContextCacheKey(prog);
       ProverContext ctx;
       ProverInterface prover;
 
-- 
cgit v1.2.3