Merge

3 files changed, 9 insertions, 21 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index dd742544..6ba49a8f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -92,7 +92,6 @@ namespace Microsoft.Boogie.SMTLib
           }

           PrepareCommon();

       }

-      prevOutcomeAvailable = false;

     }

 

     void SetupProcess()

@@ -556,13 +555,6 @@ namespace Microsoft.Boogie.SMTLib
 

     private Outcome GetResponse()

     {

-      if (prevOutcomeAvailable)

-      {

-          Contract.Assert(CommandLineOptions.Clo.StratifiedInlining > 0);

-          prevOutcomeAvailable = false;

-          return prevOutcome;

-      }

-

       var result = Outcome.Undetermined;

       var wasUnknown = false;

 

@@ -785,8 +777,6 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void Check()

     {

-        Contract.Assert(prevOutcomeAvailable == false);

-

         PrepareCommon();

         SendThisVC("(check-sat)");

         FlushLogFile();

@@ -800,14 +790,10 @@ namespace Microsoft.Boogie.SMTLib
     /// <summary>

     /// Extra state for ApiChecker (used by stratifiedInlining)

     /// </summary>

-    bool prevOutcomeAvailable;

-    Outcome prevOutcome;

     static int nameCounter = 0;

 

-    public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

+    public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

     {

-        Contract.Assert(prevOutcomeAvailable == false);

-

         unsatCore = new List<int>();

 

         // Name the assumptions

@@ -824,12 +810,13 @@ namespace Microsoft.Boogie.SMTLib
         }

         Check();

 

-        prevOutcome = GetResponse();

-        prevOutcomeAvailable = true;

+        var prevOutcome = GetResponse();

+        

         if (prevOutcome != Outcome.Valid)

         {

-            return;

+            return prevOutcome;

         }

+

         Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores");

         SendThisVC("(get-unsat-core)");

         var resp = Process.GetProverResponse();

@@ -838,6 +825,8 @@ namespace Microsoft.Boogie.SMTLib
         foreach (var s in resp.Arguments) unsatCore.Add(nameToAssumption[s.Name]);

 

         FlushLogFile();

+

+        return prevOutcome;

     }

 

     public override void Push()

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 5702111d..832d4430 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -824,7 +824,7 @@ namespace Microsoft.Boogie {
     }

 

     // (check-sat + get-unsat-core)

-    public virtual void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

+    public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

     {

         throw new NotImplementedException();

     }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fd153e11..013d7900 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1161,8 +1161,7 @@ namespace VC
 

             TheoremProver.Push();

             TheoremProver.AssertAxioms();

-            TheoremProver.CheckAssumptions(assumptions, out unsatCore);

-            ProverInterface.Outcome outcome = TheoremProver.CheckOutcomeCore(reporter);

+            ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(assumptions, out unsatCore);

             TheoremProver.Pop();

             numQueries++;