diff --git a/Source/Core/AsyncQueue.cs b/Source/Core/AsyncQueue.cs
index 787f648a1..38bc3a590 100644
--- a/Source/Core/AsyncQueue.cs
+++ b/Source/Core/AsyncQueue.cs
@@ -36,6 +36,17 @@ public void Enqueue(T value)
     }
   }
 
+  public IEnumerable<T> Items
+  {
+    get
+    {
+      lock (myLock)
+      {
+        return items.ToArray();
+      }
+    }
+  }
+
   public Task<T> Dequeue(CancellationToken cancellationToken)
   {
     lock (myLock) {
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index 397fe202f..48ce71ff3 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>2.16.3</Version>
+    <Version>2.16.4</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>
diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
new file mode 100644
index 000000000..83cd1f1ea
--- /dev/null
+++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
@@ -0,0 +1,69 @@
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace Microsoft.Boogie;
+
+/// <summary>
+/// Uses a thread pool of a configurable size, with threads with a configurable stack size,
+/// to queue tasks.
+/// </summary>
+public class CustomStackSizePoolTaskScheduler : TaskScheduler, IDisposable
+{
+  private readonly int threadCount;
+  private readonly AsyncQueue<Task> queue = new();
+  private readonly Thread[] threads;
+
+  public static CustomStackSizePoolTaskScheduler Create(int stackSize, int threadCount)
+  {
+    return new CustomStackSizePoolTaskScheduler(stackSize, threadCount);
+  }
+  
+  private CustomStackSizePoolTaskScheduler(int stackSize, int threadCount)
+  {
+    this.threadCount = threadCount;
+
+    threads = new Thread[this.threadCount];
+    for (int i = 0; i < threads.Length; i++)
+    {
+      threads[i] = new Thread(WorkLoop, stackSize) { IsBackground = true };
+      threads[i].Start();
+    }
+  }
+
+  protected override void QueueTask(Task task)
+  {
+    queue.Enqueue(task);
+  }
+
+  protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
+  {
+    return TryExecuteTask(task);
+  }
+
+  public override int MaximumConcurrencyLevel => threadCount;
+
+  protected override IEnumerable<Task> GetScheduledTasks()
+  {
+    return queue.Items;
+  }
+  
+  private void WorkLoop()
+  {
+    while (true)
+    {
+      var task = queue.Dequeue(CancellationToken.None).Result;
+      TryExecuteTask(task);
+    }
+  }
+
+  public void Dispose()
+  {
+    foreach (var thread in threads)
+    {
+      thread.Join();
+    }
+  }
+}
\ No newline at end of file
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 6de96eea3..3e2e8d357 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -26,10 +26,15 @@ public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
 
   public class ExecutionEngine : IDisposable
   {
+    /// <summary>
+    /// 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;
 
     static int autoRequestIdCount;
 
-    static readonly string AutoRequestIdPrefix = "auto_request_id_";
+    private const string AutoRequestIdPrefix = "auto_request_id_";
 
     public static string FreshRequestId() {
       var id = Interlocked.Increment(ref autoRequestIdCount);
@@ -63,6 +68,9 @@ public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache c
       Cache = cache;
       checkerPool = new CheckerPool(options);
       verifyImplementationSemaphore = new SemaphoreSlim(Options.VcsCores);
+      
+      var largeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, Options.VcsCores);
+      largeThreadTaskFactory = new(CancellationToken.None, TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, largeThreadScheduler);
     }
 
     public static ExecutionEngine CreateWithoutSharedCache(ExecutionEngineOptions options) {
@@ -870,7 +878,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
       var verificationResult = new VerificationResult(impl, programId);
 
       var batchCompleted = new Subject<(Split split, VCResult vcResult)>();
-      var completeVerification = Task.Run(async () =>
+      var completeVerification = largeThreadTaskFactory.StartNew(async () =>
       {
         var vcgen = new VCGen(processedProgram.Program, checkerPool);
         vcgen.CachingActionCounts = stats.CachingActionCounts;
@@ -931,7 +939,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
 
         batchCompleted.OnCompleted();
         return new Completed(verificationResult);
-      }, cancellationToken);
+      }, cancellationToken).Unwrap();
 
       return batchCompleted.Select(t => new BatchCompleted(t.split, t.vcResult)).Merge<IVerificationStatus>(Observable.FromAsync(() => completeVerification));
     }
diff --git a/Test/stackoverflow/nesting.bpl b/Test/stackoverflow/nesting.bpl
index 2178a6045..cf4c9f020 100644
--- a/Test/stackoverflow/nesting.bpl
+++ b/Test/stackoverflow/nesting.bpl
@@ -1,5 +1,10 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
+
+type Ref;
+type Field A B;
+type HeapType = <A, B> [Ref, Field A B]B; // Using type parameters and the ==> operator can trigger the OpTypeEraser visitor which can cause stack overflows.
+
 procedure foo(n: int)
   requires true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true
   || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true ||
@@ -14,6 +19,43 @@ procedure foo(n: int)
           true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true
             || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true ||
             n == 2;
+  requires true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+  ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+  true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+    ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+    true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+      ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+      true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+        ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+        true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+          ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+          true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+            ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+            ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+              ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+              true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                  ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                  true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                    ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                    true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                      ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                      true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                        ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                        ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                          ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                          true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                            ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                            true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                              ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                              true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                                ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                                true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                                  ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                                  true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                                    ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true;
+                                    
 {
   if (n == 2) {
     if (n == 2) {
diff --git a/Test/stackoverflow/nesting.bpl.expect b/Test/stackoverflow/nesting.bpl.expect
index 5e5ed1ea9..50f0657eb 100644
--- a/Test/stackoverflow/nesting.bpl.expect
+++ b/Test/stackoverflow/nesting.bpl.expect
@@ -1,21 +1,21 @@
-nesting.bpl(46,35): Error: this assertion could not be proved
+nesting.bpl(88,35): Error: this assertion could not be proved
 Execution trace:
-    nesting.bpl(18,3): anon0
-    nesting.bpl(19,5): anon17_Then
-    nesting.bpl(20,7): anon18_Then
-    nesting.bpl(21,9): anon19_Then
-    nesting.bpl(22,11): anon20_Then
-    nesting.bpl(23,13): anon21_Then
-    nesting.bpl(24,15): anon22_Then
-    nesting.bpl(25,17): anon23_Then
-    nesting.bpl(26,19): anon24_Then
-    nesting.bpl(27,21): anon25_Then
-    nesting.bpl(28,23): anon26_Then
-    nesting.bpl(29,25): anon27_Then
-    nesting.bpl(30,27): anon28_Then
-    nesting.bpl(31,29): anon29_Then
-    nesting.bpl(32,31): anon30_Then
-    nesting.bpl(33,33): anon31_Then
-    nesting.bpl(46,35): anon32_Then
+    nesting.bpl(60,3): anon0
+    nesting.bpl(61,5): anon17_Then
+    nesting.bpl(62,7): anon18_Then
+    nesting.bpl(63,9): anon19_Then
+    nesting.bpl(64,11): anon20_Then
+    nesting.bpl(65,13): anon21_Then
+    nesting.bpl(66,15): anon22_Then
+    nesting.bpl(67,17): anon23_Then
+    nesting.bpl(68,19): anon24_Then
+    nesting.bpl(69,21): anon25_Then
+    nesting.bpl(70,23): anon26_Then
+    nesting.bpl(71,25): anon27_Then
+    nesting.bpl(72,27): anon28_Then
+    nesting.bpl(73,29): anon29_Then
+    nesting.bpl(74,31): anon30_Then
+    nesting.bpl(75,33): anon31_Then
+    nesting.bpl(88,35): anon32_Then
 
 Boogie program verifier finished with 0 verified, 1 error