From 06771adc7acf710f055bfeeedc2c604c75ce945b Mon Sep 17 00:00:00 2001
From: Pantazis Deligiannis <pdeligia@me.com>
Date: Mon, 30 Sep 2013 09:59:01 +0100
Subject: changes to support a configured errorLimit

---
 Source/Provers/SMTLib/ProverInterface.cs | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'Source/Provers/SMTLib')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 95662d84..4a5d23d6 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -793,11 +793,11 @@ namespace Microsoft.Boogie.SMTLib
     }
 
     [NoDefaultContract]
-    public override Outcome CheckOutcome(ErrorHandler handler)
+    public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1)
     {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
 
-      var result = CheckOutcomeCore(handler);
+      var result = CheckOutcomeCore(handler, taskID: taskID);
       SendThisVC("(pop 1)");
       FlushLogFile();
 
@@ -805,7 +805,7 @@ namespace Microsoft.Boogie.SMTLib
     }
 
     [NoDefaultContract]
-    public override Outcome CheckOutcomeCore(ErrorHandler handler)
+    public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)
     {  
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
       
@@ -819,6 +819,10 @@ namespace Microsoft.Boogie.SMTLib
         FlushProverWarnings();
 
         var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
+        if (taskID >= 0) {
+          errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;
+        }
+
         if (errorsLeft < 1)
           errorsLeft = 1;
 
@@ -1314,7 +1318,7 @@ namespace Microsoft.Boogie.SMTLib
             i++;
         }
         Check();
-
+        
         var outcome = CheckOutcomeCore(handler);
 
         if (outcome != Outcome.Valid) {
-- 
cgit v1.2.3