summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-10-02 22:27:35 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-10-02 22:27:35 +0100
commit3297f35c08738cd95bd01c1f4ab1e8baadddf67e (patch)
tree58adb68086eb78112a55005892fc53e749ff036d /Source/Provers
parent2a32d6e6a9b7e193c7a49893acc52397f1824d1d (diff)
small refactoring
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs4
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 4a5d23d6..b46e6fea 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -819,7 +819,9 @@ namespace Microsoft.Boogie.SMTLib
FlushProverWarnings();
var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
- if (taskID >= 0) {
+
+ if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;
}