summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine/ExecutionEngine.cs
diff options
context:
space:
mode:
authorGravatar RustanLeino <leino@microsoft.com>2016-08-01 15:31:24 -0700
committerGravatar GitHub <noreply@github.com>2016-08-01 15:31:24 -0700
commit014e558e87572baadca1a09ad46f221d88da82b0 (patch)
tree3d06ac193219915b2f43320bd91402115b44fa05 /Source/ExecutionEngine/ExecutionEngine.cs
parent0632d3956b7cd10cdc4975cdfc669b73892a121d (diff)
parent2edc4a4e70b9dcf6fc91ddcc07fd500b705de5d2 (diff)
Merge pull request #41 from BarryBo/master
Run Boogie code on threads with large stacks
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs4
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 9bc855be..5a22cc15 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -443,6 +443,8 @@ namespace Microsoft.Boogie
static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
+ static ThreadTaskScheduler Scheduler = new ThreadTaskScheduler(16 * 1024 * 1024);
+
public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)
{
Contract.Requires(cce.NonNullElements(fileNames));
@@ -977,7 +979,7 @@ namespace Microsoft.Boogie
{
break;
}
- tasks[j].Start(TaskScheduler.Default);
+ tasks[j].Start(Scheduler);
}
// Don't wait for tasks that haven't been started yet.