Use large stack for verification task execution

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.2.2</Version>
+    <Version>3.2.3</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/ExecutionEngine/ExecutionEngine.cs

@@ -24,7 +24,7 @@ public class ExecutionEngine : IDisposable
     /// Boogie traverses the Boogie and VCExpr AST using the call-stack,
     /// so it needs to use a large stack to prevent stack overflows.
     /// </summary>
-    private readonly TaskFactory largeThreadTaskFactory;
+    public TaskFactory LargeThreadTaskFactory { get; }
 
     static int autoRequestIdCount;
 
@@ -60,7 +60,7 @@ public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache c
 
       largeThreadScheduler = scheduler;
       this.disposeScheduler = disposeScheduler;
-      largeThreadTaskFactory = new(CancellationToken.None, TaskCreationOptions.None, TaskContinuationOptions.None, largeThreadScheduler);
+      LargeThreadTaskFactory = new(CancellationToken.None, TaskCreationOptions.None, TaskContinuationOptions.None, largeThreadScheduler);
     }
 
     public static ExecutionEngine CreateWithoutSharedCache(ExecutionEngineOptions options) {
@@ -581,32 +581,40 @@ public async Task<PipelineOutcome> InferAndVerify(
 
     private ProcessedProgram PreProcessProgramVerification(Program program)
     {
-      // Doing lambda expansion before abstract interpretation means that the abstract interpreter
-      // never needs to see any lambda expressions.  (On the other hand, if it were useful for it
-      // to see lambdas, then it would be better to more lambda expansion until after inference.)
-      if (Options.ExpandLambdas) {
-        LambdaHelper.ExpandLambdas(Options, program);
-        if (Options.PrintFile != null && Options.PrintLambdaLifting) {
-          PrintBplFile(Options.PrintFile, program, false, true, Options.PrettyPrint);
+      return LargeThreadTaskFactory.StartNew(() =>
+      {
+        // Doing lambda expansion before abstract interpretation means that the abstract interpreter
+        // never needs to see any lambda expressions.  (On the other hand, if it were useful for it
+        // to see lambdas, then it would be better to more lambda expansion until after inference.)
+        if (Options.ExpandLambdas)
+        {
+          LambdaHelper.ExpandLambdas(Options, program);
+          if (Options.PrintFile != null && Options.PrintLambdaLifting)
+          {
+            PrintBplFile(Options.PrintFile, program, false, true, Options.PrettyPrint);
+          }
         }
-      }
 
-      if (Options.UseAbstractInterpretation) {
-        new AbstractInterpretation.NativeAbstractInterpretation(Options).RunAbstractInterpretation(program);
-      }
+        if (Options.UseAbstractInterpretation)
+        {
+          new AbstractInterpretation.NativeAbstractInterpretation(Options).RunAbstractInterpretation(program);
+        }
 
-      if (Options.LoopUnrollCount != -1) {
-        program.UnrollLoops(Options.LoopUnrollCount, Options.SoundLoopUnrolling);
-      }
+        if (Options.LoopUnrollCount != -1)
+        {
+          program.UnrollLoops(Options.LoopUnrollCount, Options.SoundLoopUnrolling);
+        }
 
-      var processedProgram = Options.ExtractLoops ? ExtractLoops(program) : new ProcessedProgram(program);
+        var processedProgram = Options.ExtractLoops ? ExtractLoops(program) : new ProcessedProgram(program);
 
-      if (Options.PrintInstrumented) {
-        program.Emit(new TokenTextWriter(Options.OutputWriter, Options.PrettyPrint, Options));
-      }
+        if (Options.PrintInstrumented)
+        {
+          program.Emit(new TokenTextWriter(Options.OutputWriter, Options.PrettyPrint, Options));
+        }
 
-      program.DeclarationDependencies = Prune.ComputeDeclarationDependencies(Options, program);
-      return processedProgram;
+        program.DeclarationDependencies = Prune.ComputeDeclarationDependencies(Options, program);
+        return processedProgram;
+      }).Result;
     }
 
     private ProcessedProgram ExtractLoops(Program program)
@@ -736,7 +744,7 @@ public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program)
           out var gotoCmdOrigins,
           out var modelViewInfo);
 
-        VerificationConditionGenerator.ResetPredecessors(run.Implementation.Blocks);
+        ConditionGeneration.ResetPredecessors(run.Implementation.Blocks);
         var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator).ToList();
         for (var index = 0; index < splits.Count; index++) {
           var split = splits[index];
@@ -909,7 +917,7 @@ private Task<ImplementationRunResult> VerifyImplementationWithoutCaching(Process
       string programId, Implementation impl, TextWriter traceWriter)
     {
 
-      var resultTask = largeThreadTaskFactory.StartNew(async () =>
+      var resultTask = LargeThreadTaskFactory.StartNew(async () =>
       {
         var verificationResult = new ImplementationRunResult(impl, programId);
         var vcGen = new VerificationConditionGenerator(processedProgram.Program, CheckerPool);

Source/ExecutionEngine/VerificationTask.cs

@@ -7,6 +7,7 @@
 using System.Reactive.Subjects;
 using System.Runtime.CompilerServices;
 using System.Threading;
+using System.Threading.Tasks;
 using VC;
 
 namespace Microsoft.Boogie;
@@ -78,7 +79,7 @@ public void Cancel() {
   private IObservable<IVerificationStatus>? StartRunIfNeeded() {
     // No other thread is running or can start, so we can safely access CacheStatus
     if (CacheStatus is Completed) {
-      return null;
+      return Observable.Return(CacheStatus);
     }
 
     // We claim the right to run.
@@ -120,14 +121,15 @@ private async IAsyncEnumerable<IVerificationStatus> StartRun([EnumeratorCancella
       yield return new Queued();
     }
     var checker = await checkerTask;
-    try {
+    try
+    {
       yield return new Running();
 
       var collector = new VerificationResultCollector(Split.Options);
-      await Split.BeginCheck(Split.Run.OutputWriter, checker, collector,
-        modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken);
+      await engine.LargeThreadTaskFactory.StartNew(() => Split.BeginCheck(Split.Run.OutputWriter, checker, collector,
+        modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken), cancellationToken).Unwrap();
 
-      await checker.ProverTask;
+      await checker.ProverTask.WaitAsync(cancellationToken);
       var result = Split.ReadOutcome(0, checker, collector);
 
       CacheStatus = new Completed(result);

Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs

@@ -341,6 +341,10 @@ procedure Foo(x: int) {
     Assert.AreEqual(null, runDuringRun2);
     var statusList2 = new List<IVerificationStatus>();
     secondStatuses.Subscribe(statusList2.Add);
+    while (statusList1.Last() is not Stale)
+    {
+      await Task.Delay(10);
+    }
     returnCheckSat.Release(2);
     var finalResult = await secondStatuses.ToTask();
     Assert.IsTrue(finalResult is Completed);