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++;