Kill {:prover "..."} attribute support; no one ever used this stuff

2 files changed, 0 insertions, 19 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);