3 files changed, 5 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 86a117c2..509f81ce 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -792,7 +792,7 @@ namespace Microsoft.Boogie.SMTLib
     /// </summary>
     static int nameCounter = 0;
 
-    public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+    public override Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
     {
         unsatCore = new List<int>();
 
@@ -810,7 +810,7 @@ namespace Microsoft.Boogie.SMTLib
         }
         Check();
 
-        var prevOutcome = GetResponse();
+        var prevOutcome = CheckOutcomeCore(handler);
         
         if (prevOutcome != Outcome.Valid)
         {
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index b5dc4d41..a1b9e38d 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -823,8 +823,8 @@ namespace Microsoft.Boogie {
         throw new NotImplementedException();
     }
 
-    // (check-sat + get-unsat-core)
-    public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+    // (check-sat + get-unsat-core + checkOutcome)
+    public virtual Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
     {
         throw new NotImplementedException();
     }
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 65660a2d..9e55b3d6 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1142,7 +1142,7 @@ namespace VC
 
             TheoremProver.Push();
             TheoremProver.AssertAxioms();
-            ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(assumptions, out unsatCore);
+            ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(assumptions, out unsatCore, reporter);
             TheoremProver.Pop();
             numQueries++;