diff options
author | Pantazis Deligiannis <pdeligia@me.com> | 2013-09-30 09:59:01 +0100 |
---|---|---|
committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-09-30 09:59:01 +0100 |
commit | 06771adc7acf710f055bfeeedc2c604c75ce945b (patch) | |
tree | 726cfd8957abcbfffcb3e76f7625bacb1d21a7d2 /Source/Provers/SMTLib/ProverInterface.cs | |
parent | 0b4388429f5eb571fce4b1aff508be891ad75b87 (diff) |
changes to support a configured errorLimit
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 12 |
1 files changed, 8 insertions, 4 deletions
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) {
|