deleted the option UseUnsatCoreForInlining

Split ApiChecker.CheckAssumptions into two different methods, one which computes the unsatCore and one which does not
Further edits to the MaxSat code

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 5e262f87..9987e6f4 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -85,7 +85,7 @@ namespace Microsoft.Boogie.SMTLib
           {

               currentLogFile = OpenOutputFile("");

           }

-          if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.UseUnsatCoreForInlining)

+          if (CommandLineOptions.Clo.ProcedureCopyBound > 0)

           {

               SendThisVC("(set-option :produce-unsat-cores true)");

               this.usingUnsatCore = true;

@@ -835,7 +835,7 @@ namespace Microsoft.Boogie.SMTLib
         DeclCollector.Push();

     }

 

-    public override Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions) {

+    public override Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions, ErrorHandler handler) {

       unsatisfiedSoftAssumptions = new List<int>();

 

       Push();

@@ -863,7 +863,7 @@ namespace Microsoft.Boogie.SMTLib
           SendThisVC("(assert " + a + ")");

         }

         Check();

-        outcome = GetResponse();

+        outcome = CheckOutcomeCore(handler);

         Pop();

         if (outcome != Outcome.Valid)

           break;