diff --git a/.gitmodules b/.gitmodules
index aa94f844181..e5dec47b942 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,6 @@
 [submodule "Test/libraries"]
 	path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
 	url = https://github.com/dafny-lang/libraries.git
+[submodule "boogie"]
+	path = boogie
+	url = git@github.com:keyboardDrummer/boogie.git
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 23297b185ed..fc8e8b1fa49 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -138,5 +164,17 @@ Global
 		SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
+		{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
 	EndGlobalSection
 EndGlobal
diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
index e1499557a15..c15a3145ea3 100644
--- a/Source/DafnyCore/DafnyCore.csproj
+++ b/Source/DafnyCore/DafnyCore.csproj
@@ -34,7 +34,17 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.1.6" />
+      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Graph\Graph.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Model\Model.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCExpr\VCExpr.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCGeneration\VCGeneration.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Houdini\Houdini.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency.csproj" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index 67b3f734b08..74acb94d988 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -71,6 +71,8 @@ static DafnyCommands() {
     Snippets.ShowSnippets,
     DeveloperOptionBag.PrintOption,
     DeveloperOptionBag.ResolvedPrint,
+    DeveloperOptionBag.SplitPrint,
+    DeveloperOptionBag.PassivePrint,
     DeveloperOptionBag.BoogiePrint,
     Printer.PrintMode,
     CommonOptionBag.AllowWarnings,
diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs
index 46e33eab351..3664718b741 100644
--- a/Source/DafnyCore/Options/DeveloperOptionBag.cs
+++ b/Source/DafnyCore/Options/DeveloperOptionBag.cs
@@ -6,6 +6,22 @@ namespace Microsoft.Dafny;
 
 public class DeveloperOptionBag {
 
+  public static readonly Option<string> SplitPrint = new("--sprint",
+    @"
+Print Boogie splits translated from Dafny
+(use - as <file> to print to console)".TrimStart()) {
+    IsHidden = true,
+    ArgumentHelpName = "file",
+  };
+  
+  public static readonly Option<string> PassivePrint = new("--pprint",
+    @"
+Print passified Boogie program translated from Dafny
+(use - as <file> to print to console)".TrimStart()) {
+    IsHidden = true,
+    ArgumentHelpName = "file",
+  };
+  
   public static readonly Option<string> BoogiePrint = new("--bprint",
   @"
 Print Boogie program translated from Dafny
@@ -48,13 +64,27 @@ static DeveloperOptionBag() {
         options.FileTimestamp);
     });
 
+    DafnyOptions.RegisterLegacyBinding(PassivePrint, (options, f) => {
+      options.PrintPassiveFile = f;
+      options.ExpandFilename(options.PrintPassiveFile, x => options.PrintPassiveFile = x, options.LogPrefix,
+        options.FileTimestamp);
+    });
+
     DafnyOptions.RegisterLegacyBinding(BoogiePrint, (options, f) => {
       options.PrintFile = f;
       options.ExpandFilename(options.PrintFile, x => options.PrintFile = x, options.LogPrefix,
         options.FileTimestamp);
     });
+    
+    DafnyOptions.RegisterLegacyBinding(SplitPrint, (options, f) => {
+      options.PrintSplitFile = f;
+      options.ExpandFilename(options.PrintSplitFile, x => options.PrintSplitFile = x, options.LogPrefix,
+        options.FileTimestamp);
+    });
 
+    DooFile.RegisterNoChecksNeeded(PassivePrint, false);
     DooFile.RegisterNoChecksNeeded(BoogiePrint, false);
+    DooFile.RegisterNoChecksNeeded(SplitPrint, false);
     DooFile.RegisterNoChecksNeeded(PrintOption, false);
     DooFile.RegisterNoChecksNeeded(ResolvedPrint, false);
     DooFile.RegisterNoChecksNeeded(Bootstrapping, false);
diff --git a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
index ed44471f310..6d276fbbdc7 100644
--- a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
+++ b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
@@ -3,9 +3,12 @@
 using System.CommandLine;
 using System.Linq;
 using System.Reactive.Subjects;
+using System.Threading;
 using System.Threading.Tasks;
 using DafnyCore;
 using DafnyDriver.Commands;
+using Microsoft.Boogie;
+using VC;
 
 namespace Microsoft.Dafny;
 
@@ -13,10 +16,12 @@ static class MeasureComplexityCommand {
   public static IEnumerable<Option> Options => new Option[] {
     Iterations,
     RandomSeed,
+    TopX,
     VerifyCommand.FilterSymbol,
     VerifyCommand.FilterPosition,
   }.Concat(DafnyCommands.VerificationOptions).
-    Concat(DafnyCommands.ResolverOptions);
+    Concat(DafnyCommands.ResolverOptions).
+    Concat(DafnyCommands.ConsoleOutputOptions);
 
   static MeasureComplexityCommand() {
     DafnyOptions.RegisterLegacyBinding(Iterations, (o, v) => o.RandomizeVcIterations = (int)v);
@@ -24,12 +29,16 @@ static MeasureComplexityCommand() {
 
     DooFile.RegisterNoChecksNeeded(Iterations, false);
     DooFile.RegisterNoChecksNeeded(RandomSeed, false);
+    DooFile.RegisterNoChecksNeeded(TopX, false);
   }
 
+  private static readonly Option<uint> TopX = new("--worst-amount", () => 10U,
+    $"Configures the amount of worst performing verification tasks that are reported.");
+
   private static readonly Option<uint> RandomSeed = new("--random-seed", () => 0U,
     $"Turn on randomization of the input that Dafny passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Dafny proofs are complex in the sense that changes to the proof that preserve its meaning may cause its verification result to change. This option simulates meaning-preserving changes to the proofs without requiring the user to actually make those changes. The proof changes are renaming variables and reordering declarations in the SMT input passed to the solver, and setting solver options that have similar effects.");
 
-  private static readonly Option<uint> Iterations = new("--iterations", () => 10U,
+  private static readonly Option<uint> Iterations = new("--iterations", () => 1U,
     $"Attempt to verify each proof n times with n random seeds, each seed derived from the previous one. {RandomSeed.Name} can be used to specify the first seed, which will otherwise be 0.") {
     ArgumentHelpName = "n"
   };
@@ -62,7 +71,7 @@ private static async Task<int> Execute(DafnyOptions options) {
       // For error diagnostics, we should group duplicates and say how often they occur.
       // Performance data of individual verification tasks (VCs) should be grouped by VcNum (the assertion batch).
       VerifyCommand.ReportVerificationDiagnostics(compilation, verificationResults);
-      var summaryReported = VerifyCommand.ReportVerificationSummary(compilation, verificationResults);
+      var summaryReported = ReportResourceSummary(compilation, verificationResults);
       var proofDependenciesReported = VerifyCommand.ReportProofDependencies(compilation, resolution, verificationResults);
       var verificationResultsLogged = VerifyCommand.LogVerificationResults(compilation, resolution, verificationResults);
 
@@ -75,13 +84,47 @@ private static async Task<int> Execute(DafnyOptions options) {
     return await compilation.GetAndReportExitCode();
   }
 
+  public static async Task ReportResourceSummary(
+    CliCompilation cliCompilation,
+    IObservable<CanVerifyResult> verificationResults) {
+
+    PriorityQueue<VerificationTaskResult, int> worstPerformers = new();
+
+    var totalResources = 0;
+    var worstAmount = cliCompilation.Options.Get(TopX);
+    verificationResults.Subscribe(result => {
+      foreach (var taskResult in result.Results) {
+        var runResult = taskResult.Result;
+        totalResources += runResult.ResourceCount;
+        worstPerformers.Enqueue(taskResult, runResult.ResourceCount);
+        if (worstPerformers.Count > worstAmount) {
+          worstPerformers.Dequeue();
+        }
+      }
+    });
+    await verificationResults.WaitForComplete();
+    var output = cliCompilation.Options.OutputWriter;
+    var decreasingWorst = new Stack<VerificationTaskResult>();
+    while (worstPerformers.Count > 0) {
+      decreasingWorst.Push(worstPerformers.Dequeue());
+    }
+
+    await output.WriteLineAsync($"The total consumed resources are {totalResources}");
+    await output.WriteLineAsync($"The most demanding {worstAmount} verification tasks consumed these resources:");
+    foreach (var performer in decreasingWorst) {
+      var location = ((IToken)performer.Task.Token).TokenToString(cliCompilation.Options);
+      await output.WriteLineAsync($"{location}: {performer.Result.ResourceCount}");
+    }
+  }
+
   private static async Task RunVerificationIterations(DafnyOptions options, CliCompilation compilation,
     IObserver<CanVerifyResult> verificationResultsObserver) {
     int iterationSeed = (int)options.Get(RandomSeed);
     var random = new Random(iterationSeed);
-    foreach (var iteration in Enumerable.Range(0, (int)options.Get(Iterations))) {
+    var iterations = (int)options.Get(Iterations);
+    foreach (var iteration in Enumerable.Range(0, iterations)) {
       await options.OutputWriter.WriteLineAsync(
-        $"Starting verification of iteration {iteration} with seed {iterationSeed}");
+        $"Starting verification of iteration {iteration + 1}/{iterations} with seed {iterationSeed}");
       try {
         await foreach (var result in compilation.VerifyAllLazily(iterationSeed)) {
           verificationResultsObserver.OnNext(result);
diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
index c10d2dbaa4d..64a9c4bb905 100644
--- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
+++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
@@ -138,8 +138,8 @@ await AssertVerificationHoverMatches(documentItem, (0, 36),
 
 - Total resource usage: ??? RU  
 - Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches):  
-  - #???/??? with 1 assertion  at line ???, ??? RU  
-  - #???/??? with 1 assertion  at line ???, ??? RU  "
+  - #???/??? with 1 assertion at line ???, ??? RU  
+  - #???/??? with 1 assertion at line ???, ??? RU"
       );
     }
 
diff --git a/Source/DafnyLanguageServer/LanguageServer.cs b/Source/DafnyLanguageServer/LanguageServer.cs
index a3fe6625527..2d15d60eebb 100644
--- a/Source/DafnyLanguageServer/LanguageServer.cs
+++ b/Source/DafnyLanguageServer/LanguageServer.cs
@@ -28,6 +28,8 @@ public class LanguageServer {
         DafnyLangSymbolResolver.UseCaching,
         ProjectManager.UpdateThrottling,
         CachingProjectFileOpener.ProjectFileCacheExpiry,
+        DeveloperOptionBag.SplitPrint,
+        DeveloperOptionBag.PassivePrint,
         DeveloperOptionBag.BoogiePrint,
         CommonOptionBag.EnforceDeterminism,
         InternalDocstringRewritersPluginConfiguration.UseJavadocLikeDocstringRewriterOption,
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect
index ef71487de53..b94f4205220 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 74 verified, 0 errors
+Dafny program verifier finished with 72 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy
new file mode 100644
index 00000000000..62e786470c7
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy
@@ -0,0 +1,20 @@
+// RUN: %exits-with 4 %baredafny measure-complexity --show-snippets false --use-basename-for-filename --isolate-assertions --worst-amount 100 "%s" > %t.raw
+// RUN: %sed 's#\): \d+#): <redacted>#g' %t.raw > %t.raw2
+// RUN: %sed 's#are \d+#are <redacted>#g' %t.raw2 > %t
+// RUN: %diff "%s.expect" "%t"
+method Foo() {
+  assert Ack(0,0) == 10;
+  assert Ack(1,3) == 10;
+  assert Ack(3,3) == 10;
+  assert Ack(3,4) == 10;
+}
+
+function Ack(m: nat, n: nat): nat
+{
+  if m == 0 then
+    n + 1
+  else if n == 0 then
+    Ack(m - 1, 1)
+  else
+    Ack(m - 1, Ack(m, n - 1))
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
new file mode 100644
index 00000000000..4ccfc445f22
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
@@ -0,0 +1,30 @@
+Starting verification of iteration 1/1 with seed 0
+measure-complexity.dfy(6,18): Error: assertion might not hold
+The total consumed resources are <redacted>
+The most demanding 100 verification tasks consumed these resources:
+measure-complexity.dfy(19,4): <redacted>
+measure-complexity.dfy(9,18): <redacted>
+measure-complexity.dfy(19,4): <redacted>
+measure-complexity.dfy(19,4): <redacted>
+measure-complexity.dfy(8,18): <redacted>
+measure-complexity.dfy(7,18): <redacted>
+measure-complexity.dfy(19,10): <redacted>
+measure-complexity.dfy(6,18): <redacted>
+measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy(19,24): <redacted>
+measure-complexity.dfy(17,10): <redacted>
+measure-complexity.dfy(15,6): <redacted>
+measure-complexity.dfy(8,15): <redacted>
+measure-complexity.dfy(9,15): <redacted>
+measure-complexity.dfy(9,13): <redacted>
+measure-complexity.dfy(7,13): <redacted>
+measure-complexity.dfy(17,15): <redacted>
+measure-complexity.dfy(8,13): <redacted>
+measure-complexity.dfy(7,15): <redacted>
+measure-complexity.dfy(6,15): <redacted>
+measure-complexity.dfy(6,13): <redacted>
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect
index 4fd36a1d403..e8941d7c746 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 597 verified, 0 errors
+Dafny program verifier finished with 595 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect
index f3e2b391bdf..77b1d1fa8a9 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 491 verified, 0 errors
+Dafny program verifier finished with 489 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect
index c2bb304608c..7a991a13c44 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 444 verified, 0 errors
+Dafny program verifier finished with 442 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect
index 0d2842886fd..0106799b5a5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect
@@ -22,4 +22,4 @@ Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreas
 Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 
-Dafny program verifier finished with 112 verified, 23 errors
+Dafny program verifier finished with 108 verified, 23 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect
index 65c547aff38..e617b14d52a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect
@@ -23,4 +23,4 @@ Termination.dfy(923,2): Error: cannot prove termination; try supplying a decreas
 Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 
-Dafny program verifier finished with 111 verified, 24 errors
+Dafny program verifier finished with 107 verified, 24 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect
index 638376bfd6c..45df7d21223 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect
@@ -7,4 +7,4 @@ MoreInduction.dfy(87,10): Related location: this is the postcondition that could
 MoreInduction.dfy(93,0): Error: a postcondition could not be proved on this return path
 MoreInduction.dfy(92,21): Related location: this is the postcondition that could not be proved
 
-Dafny program verifier finished with 28 verified, 4 errors
+Dafny program verifier finished with 26 verified, 4 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy
index e6b4d5b59b0..a95f9dd5df5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy
@@ -214,11 +214,18 @@ ghost function IntRange(lo: nat, len: nat): set<nat>
   S
 }
 
+lemma BoundedSetSize(xs: set<nat>, lower: nat, upper: nat)
+  requires forall x <- xs :: lower <= x && x < upper
+  ensures |xs| <= upper - lower
+
 // ----- Proofs of alternative versions
 
 lemma {:isolate_assertions} SMN'_Correct(xs: List<nat>, n: nat, len: nat)
   requires NoDuplicates(xs)
+// a
   requires forall x :: x in Elements(xs) ==> n <= x
+// b
+// c
   requires len == Length(xs)
   ensures var s := SMN'(xs, n, len);
     n <= s <= n + len &&
@@ -239,6 +246,16 @@ lemma {:isolate_assertions} SMN'_Correct(xs: List<nat>, n: nat, len: nat)
       SMN'_Correct(L, n, llen);
     } else {
       var s := SMN'(R, n + llen, len - llen);
+      // at worst the elements in L are consecutive, and then the lower bound of R is n + llen
+      // elements in R are bigger than those in L
+      // the biggest element in L is n + half
+      // assert llen >= half;
+
+      assert llen == half by {
+        BoundedSetSize(Elements(L), n, n + half);
+        assert |Elements(L)| <= (n + half) - n;
+        assert |Elements(L)| <= half;    
+      }
       SMN'_Correct(R, n + llen, len - llen);
       forall x | n <= x < s
         ensures x in Elements(xs)
@@ -274,6 +291,12 @@ lemma {:isolate_assertions} SMN''_Correct(xs: List<nat>, n: nat, len: nat)
       SMN''_Correct(L, n, llen);
     } else {
       var s := SMN''(R, n + llen, len - llen);
+
+      assert llen == half by {
+        BoundedSetSize(Elements(L), n, n + half);
+        assert |Elements(L)| <= (n + half) - n;
+        assert |Elements(L)| <= half;    
+      }
       SMN''_Correct(R, n + llen, len - llen);
       forall x | n <= x < s
         ensures x in Elements(xs)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect
index 023b0990012..b49c1470365 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 33 verified, 0 errors
+Dafny program verifier finished with 32 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect
index 35e54b59f6f..e7cc92d0e90 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect
@@ -1,3 +1,3 @@
 SoftwareFoundations-Basics.dfy(41,11): Error: assertion might not hold
 
-Dafny program verifier finished with 53 verified, 1 error
+Dafny program verifier finished with 52 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy
index 9c23169829f..f0287b98ef4 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy
@@ -192,7 +192,7 @@ class Memory {
     twostate predicate {:opaque}     {:no_inline} Valid2()
         reads this`objects, objects, objects`fields
         ensures Valid2() ==> Valid()
-    { 
+    {
      reveal Valid();
      Valid()
        &&
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
index efc7dd6b97d..4179629fa5d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
@@ -7,4 +7,4 @@ git-issue-3855.dfy(434,36): Related location: this is the precondition that coul
 git-issue-3855.dfy(1337,20): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved
 
-Dafny program verifier finished with 101 verified, 3 errors, 1 time out
+Dafny program verifier finished with 99 verified, 3 errors, 1 time out
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
index a7d4037754a..a360a1d34af 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
@@ -2,4 +2,4 @@ ArrowTypeOptimizations.dfy(10,2): Error: function precondition could not be prov
 ArrowTypeOptimizations.dfy(10,2): Error: insufficient reads clause to invoke function
 ArrowTypeOptimizations.dfy(16,2): Error: function precondition could not be proved
 
-Dafny program verifier finished with 17 verified, 3 errors
+Dafny program verifier finished with 10 verified, 3 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect
index caca1722291..36b67dbf599 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 47 verified, 0 errors
+Dafny program verifier finished with 46 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
index 30b324a028a..9aada7e7404 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy
@@ -2,8 +2,8 @@
 // Also test old CLI
 // RUN: %exits-with 4 %baredafny /compile:0 /verificationLogger:json /vcsSplitOnEveryAssert "%s" >> "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid
-// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid
+// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:2,.outcome.:.Invalid
+// CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:2,.outcome.:.Invalid
 method M(x: int, y: int)
   requires y > 0
   requires x > 0
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check
index 90c7b48aea4..f93bddb3848 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check
@@ -1,26 +1,24 @@
 CHECK: Verified 0/2 symbols. Waiting for f to verify.
-CHECK: Verification part 1/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 2/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 3/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 4/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 5/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 6/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 7/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 8/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 9/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 10/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 11/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 1/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 2/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 3/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 4/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 5/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 6/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 7/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 8/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 9/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 10/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
 CHECK: Verified 1/2 symbols. Waiting for L to verify.
-CHECK: Verification part 1/9 of L, on line 7, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 2/9 of L, on line 9, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 3/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 4/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 5/9 of L, on line 10, ran out of resources \(time: .*, resource count: .*\)
-CHECK: Verification part 6/9 of L, on line 11, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 7/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 8/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
-CHECK: Verification part 9/9 of L, on line 12, ran out of resources
+CHECK: Verification part 1/8 of L, on line 9, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 2/8 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 3/8 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 4/8 of L, on line 10, ran out of resources \(time: .*, resource count: .*\)
+CHECK: Verification part 5/8 of L, on line 11, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 6/8 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 7/8 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 8/8 of L, on line 12, ran out of resources
 outOfResourceAndIsolateAssertions.dfy\(10,18\): Error: Verification out of resource \(L\)
 outOfResourceAndIsolateAssertions.dfy\(12,18\): Error: Verification out of resource \(L\)
 
-Dafny program verifier finished with 18 verified, 0 errors, 2 out of resource
+Dafny program verifier finished with 16 verified, 0 errors, 2 out of resource
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
index 5d27b222f10..990ff81151d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
@@ -1,12 +1,7 @@
-// CHECK:Verification part 1/3 of Foo, on line 6, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 2/3 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 3/3 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 1/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 2/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 1/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 2/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 1/3 of Burp, on line 16, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 2/3 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 3/3 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 1/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 2/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/1 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/1 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/1 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
index 9f99b707598..df0d3e19d23 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
@@ -1,8 +1,7 @@
 // RUN: %verify --progress --cores=1 %s &> %t
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK:Verification part 1/3 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 2/3 of Foo, on line 11, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verification part 3/3 of Foo, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Foo, on line 11, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Foo, on line 12, verified successfully \(time: .*, resource count: .*\)
 // CHECK:Verified 1/2 symbols. Waiting for Bar to verify.
 // CHECK:Verification part 1/1 of Bar, on line 15, verified successfully \(time: .*, resource count: .*\)
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect
index 5436a7e7dc4..6fcd2337d72 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 164 verified, 0 errors
+Dafny program verifier finished with 161 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect
index 42324885fd1..3b71b05bfb8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 56 verified, 0 errors
+Dafny program verifier finished with 55 verified, 0 errors
diff --git a/boogie b/boogie
new file mode 160000
index 00000000000..97fbea55254
--- /dev/null
+++ b/boogie
@@ -0,0 +1 @@
+Subproject commit 97fbea552542bf3516f2c4098ad290016e2b3b86
diff --git a/docs/dev/news/5631.feat b/docs/dev/news/5631.feat
new file mode 100644
index 00000000000..70a4d27e91a
--- /dev/null
+++ b/docs/dev/news/5631.feat
@@ -0,0 +1,5 @@
+Let the command `measure-complexity` output which verification tasks performed the worst in terms of resource count. Output looks like:
+...
+Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources
+Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources
+...
\ No newline at end of file