3 files changed, 0 insertions, 66 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 8540fc62..50eefc49 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -415,9 +415,6 @@ namespace Microsoft.Boogie.Simplify {
         int num_axioms_pushed =
            FeedNewAxiomsDecls2Prover();
 
-        string prelude = ctx.GetProverCommands(false);
-        Contract.Assert(prelude != null);
-        vcString = prelude + vcString;
         LogActivity(vcString);
 
         Contract.Assert(thmProver != null);
@@ -557,19 +554,11 @@ namespace Microsoft.Boogie.Simplify {
         thmProver.Feed(parmsetting, 0);
       }
       thmProver.Feed(GetBackgroundPredicate(BackgroundPredFilename), 3);
-      string incProverCommands = ctx.GetProverCommands(false);
-      Contract.Assert(incProverCommands != null);
-      string proverCommands = ctx.GetProverCommands(true);
-      Contract.Assert(proverCommands != null);
-      string prelude = ctx.GetProverCommands(false);
-      Contract.Assert(prelude != null);
 
       if (restarts == 0) {
         // log the stuff before feeding it into the prover, so when it dies
         // and takes Boogie with it, we know what happened
         LogCommon(GetBackgroundPredicate(BackgroundPredFilename));
-        LogCommon(prelude);
-        LogCommon(proverCommands);
 
         foreach (string s in vcExprTranslator.AllTypeDecls){Contract.Assert(s != null);
           LogCommon(s);}
@@ -577,13 +566,8 @@ namespace Microsoft.Boogie.Simplify {
           LogBgPush(s);}
 
         LogCommonComment("Initialized all axioms.");
-      } else {
-        LogCommon(incProverCommands);
       }
 
-      thmProver.Feed(prelude, 0);
-      thmProver.Feed(proverCommands, 0);
-
       foreach (string s in vcExprTranslator.AllTypeDecls){Contract.Assert(s != null);
         thmProver.Feed(s, 0);}
       foreach (string s in vcExprTranslator.AllAxioms){Contract.Assert(s != null);
diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index ba4e406b..d18535e2 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -148,9 +148,6 @@ USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool
       }
 
       string vcString = "fof(vc, conjecture, " + VCExpr2String(vc, 1) + ").";
-      string prelude = ctx.GetProverCommands(true);
-      Contract.Assert(prelude != null);
-      WriteLineAndLog(output, prelude);
 
       foreach (string s in TypeDecls) {
         Contract.Assert(s != null);
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index ac52111e..6e7ba92a 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -80,9 +80,6 @@ public abstract class ProverContextContracts:ProverContext{
     
     protected OrderingAxiomBuilder orderingAxiomBuilder;
 
-    StringBuilder proverCommands;
-    StringBuilder incrementalProverCommands;
-    
     protected List<Variable> distincts;
     protected List<VCExpr> axiomConjuncts;
 
@@ -92,8 +89,6 @@ public abstract class ProverContextContracts:ProverContext{
       Contract.Invariant(genOptions != null);
       Contract.Invariant(translator != null);
       Contract.Invariant(orderingAxiomBuilder != null);
-      Contract.Invariant(proverCommands != null);
-      Contract.Invariant(incrementalProverCommands != null);
       Contract.Invariant(cce.NonNullElements(distincts));
       Contract.Invariant(cce.NonNullElements(axiomConjuncts));
     }
@@ -113,9 +108,6 @@ public abstract class ProverContextContracts:ProverContext{
       oab.Setup();
       this.orderingAxiomBuilder = oab;
 
-      proverCommands = new StringBuilder();
-      incrementalProverCommands = new StringBuilder();
-    
       distincts = new List<Variable>();
       axiomConjuncts = new List<VCExpr>();
 
@@ -133,12 +125,6 @@ public abstract class ProverContextContracts:ProverContext{
 
       StringBuilder cmds = new StringBuilder ();
       
-      cmds.Append(ctxt.proverCommands);
-      proverCommands = cmds;
-      StringBuilder incCmds = new StringBuilder ();
-      incCmds.Append(ctxt.incrementalProverCommands);
-      incrementalProverCommands = incCmds;
-    
       distincts = new List<Variable>(ctxt.distincts);
       axiomConjuncts = new List<VCExpr>(ctxt.axiomConjuncts);
 
@@ -154,32 +140,6 @@ public abstract class ProverContextContracts:ProverContext{
       return new DeclFreeProverContext(this);
     }
 
-    internal protected void SayToProver(string msg)
-    {
-      Contract.Requires(msg != null);
-      msg = msg + "\r\n";
-      proverCommands.Append(msg);
-      incrementalProverCommands.Append(msg);
-    }
-
-    protected override void ProcessDeclaration(Declaration decl)
-    {
-      //Contract.Requires(decl != null);
-      for (QKeyValue a = decl.Attributes; a != null; a = a.Next) {
-        if (a.Key == "prover" && a.Params.Count == 1) {
-          string cmd = a.Params[0] as string;
-          if (cmd != null) {
-            int pos = cmd.IndexOf(':');
-            if (pos <= 0)
-              throw new ProverException("Invalid syntax of :prover string: `" + cmd + "'");
-            string kind = cmd.Substring(0, pos);
-            if (genOptions.IsAnyProverCommandSupported(kind))
-              SayToProver(cmd.Substring(pos + 1));
-          }
-        }
-      }
-    }
-    
     public override void DeclareFunction(Function f, string attributes) {//Contract.Requires(f != null);
       base.ProcessDeclaration(f);
     }
@@ -225,13 +185,6 @@ public abstract class ProverContextContracts:ProverContext{
       }
     }
 
-    public string GetProverCommands(bool full) {Contract.Ensures(Contract.Result<string>() != null);
-
-      string res = (full ? proverCommands : incrementalProverCommands).ToString();
-      incrementalProverCommands.Length = 0;
-      return res;
-    }
-
     public override string Lookup(VCExprVar var)
     {
         return exprTranslator.Lookup(var);