Boogie: internal clean-up, removed BvHandling type, everything now behaves as if the old /bv:z were used

1 files changed, 5 insertions, 16 deletions

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;