Update Boogie to 3.2.4 (dafny-lang#5709)

### Description - Update Boogie to 3.2.4 ### How has this been tested? - Updated test expect files <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dnezam · Sep 21, 2024 · f1be5cb · f1be5cb
1 parent 6c9e016
commit f1be5cb
Show file tree

Hide file tree

Showing 40 changed files with 70 additions and 71 deletions.
diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
@@ -34,7 +34,7 @@
       <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.2.3" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs
@@ -575,7 +575,7 @@ public static VcOutcome GetOutcome(SolverOutcome outcome) {
       case SolverOutcome.Undetermined:
         return VcOutcome.Inconclusive;
       case SolverOutcome.Bounded:
-        return VcOutcome.ReachedBound;
+        return VcOutcome.Correct;
       default:
         throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null);
     }

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
@@ -189,7 +189,7 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
           var runResult = completed.Result;
           var timeString = runResult.RunTime.ToString("g");
           Options.OutputWriter.WriteLine(
-            $"Verification part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
+            $"Verified part #{boogieUpdate.VerificationTask.Split.SplitIndex}, {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
             $", on line {token.line}, " +
             $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" +
             $" (time: {timeString}, resource count: {runResult.ResourceCount})");

diff --git 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/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs
@@ -62,7 +62,7 @@ public async Task<IReadOnlyList<IVerificationTask>> GetVerificationTasksAsync(Ex
           ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint);
         }
 
-        return engine.GetVerificationTasks(boogieProgram);
+        return await engine.GetVerificationTasks(boogieProgram, cancellationToken);
       }
       finally {
         mutex.Release();

diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/UnicodeStringsWithUnicodeChar.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/UnicodeStringsWithUnicodeChar.dfy
@@ -25,6 +25,7 @@ module Std.Unicode.UnicodeStringsWithUnicodeChar refines AbstractUnicodeStrings
     // but is clearly true given the above.
     assume {:axiom} c as int as bv24 < 0x11_0000 as bv24;
     var asBits := c as int as bv24;
+    assert asBits < 0x11_0000 as bv24;
     assert (asBits < Base.HIGH_SURROGATE_MIN || asBits > Base.LOW_SURROGATE_MAX);
     assert asBits <= 0x10_FFFF;
   }

diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy
@@ -231,7 +231,7 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm {
   }
 
   function
-    {:resource_limit 4000000}
+    {:isolate_assertions}
   DecodeMinimalWellFormedCodeUnitSubsequenceQuadrupleByte(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue)
     requires |m| == 4
     ensures 0x10000 <= v <= 0x10FFFF
@@ -247,6 +247,11 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm {
     var y := (thirdByte & 0x3F) as bv24;
     var x := (fourthByte & 0x3F) as bv24;
     assert {:split_here} true;
-    (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as ScalarValue
+    var r := (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as ScalarValue;
+    assert EncodeScalarValueQuadrupleByte(r)[0] == m[0];
+    assert EncodeScalarValueQuadrupleByte(r)[1] == m[1];
+    assert EncodeScalarValueQuadrupleByte(r)[2] == m[2];
+    assert EncodeScalarValueQuadrupleByte(r)[3] == m[3];
+    r
   }
 }
diff --git 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/ast/reveal/focus.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 43 verified, 0 errors
+Dafny program verifier finished with 20 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect
@@ -1,3 +1,3 @@
 revealConstants.dfy(10,19): Error: assertion might not hold
 
-Dafny program verifier finished with 5 verified, 1 error
+Dafny program verifier finished with 3 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect
@@ -2,4 +2,4 @@ revealFunctions.dfy(15,12): Error: assertion might not hold
 revealFunctions.dfy(22,12): Error: assertion might not hold
 revealFunctions.dfy(49,21): Error: assertion might not hold
 
-Dafny program verifier finished with 26 verified, 3 errors
+Dafny program verifier finished with 14 verified, 3 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect
@@ -9,4 +9,4 @@ revealInBlock.dfy(81,10): Error: assertion might not hold
 revealInBlock.dfy(91,14): Error: assertion might not hold
 revealInBlock.dfy(94,10): Error: assertion might not hold
 
-Dafny program verifier finished with 26 verified, 10 errors
+Dafny program verifier finished with 19 verified, 10 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
@@ -21,12 +21,10 @@ measure-complexity.dfy(19,4): <redacted>
 measure-complexity.dfy(19,4): <redacted>
 measure-complexity.dfy(9,13): <redacted>
 measure-complexity.dfy(17,4): <redacted>
-measure-complexity.dfy(6,13): <redacted>
 measure-complexity.dfy(8,15): <redacted>
-measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(6,13): <redacted>
 measure-complexity.dfy(8,13): <redacted>
+measure-complexity.dfy(17,4): <redacted>
 measure-complexity.dfy(19,15): <redacted>
 measure-complexity.dfy(6,15): <redacted>
 measure-complexity.dfy(19,15): <redacted>
-measure-complexity.dfy(12,9): <redacted>
-measure-complexity.dfy(5,7): <redacted>
diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect b/...tegrationTests/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 590 verified, 0 errors
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect b/...e/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 486 verified, 0 errors
diff --git a/...IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect b/...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 434 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
@@ -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
@@ -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
@@ -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/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/.../IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect b/.../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.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(1335,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
@@ -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
@@ -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
@@ -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/...ts/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check b/...ts/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check
@@ -1,25 +1,23 @@
 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: Verified part #0, 1/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #1, 2/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #2, 3/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #3, 4/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #4, 5/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #5, 6/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #6, 7/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #7, 8/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #8, 9/10 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #9, 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: Verified part #0, 1/8 of L, on line 9, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #1, 2/8 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #2, 3/8 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #3, 4/8 of L, on line 10, ran out of resources \(time: .*, resource count: .*\)
+CHECK: Verified part #4, 5/8 of L, on line 11, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #5, 6/8 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #6, 7/8 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified part #7, 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\)
 

diff --git a/...egrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check b/...egrationTests/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:Verified part #0, 1/2 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #1, 2/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #0, 1/1 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #0, 1/1 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #0, 1/2 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #1, 2/2 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #0, 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
@@ -1,11 +1,9 @@
 // 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:Verified part #0, 1/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified part #1, 2/2 of Foo, on line 10, 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: .*\)
-
+// CHECK:Verified part #0, 1/1 of Bar, on line 13, verified successfully \(time: .*, resource count: .*\)
 
 method {:isolate_assertions} Foo() {
   assert true;

diff --git 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 142 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
@@ -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/customBoogie.patch b/customBoogie.patch
@@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
        <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.2.3" />
+-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
@@ -448,6 +448,10 @@ Usage: dafny [ option ... ] [ filename ... ]
 
   /loopUnroll:<n>
                 unroll loops, following up to n back edges (and then some)
+                default is -1, which means loops are not unrolled
+  /extractLoops
+                extract reducible loops into recursive procedures and
+                inline irreducible loops using the bound supplied by /loopUnroll:<n>
   /soundLoopUnrolling
                 sound loop unrolling
   /doModSetAnalysis

diff --git a/docs/DafnyRef/Statements.8b.expect b/docs/DafnyRef/Statements.8b.expect
@@ -1,4 +1,4 @@
 text.dfy(6,12): Error: function precondition could not be proved
 text.dfy(3,30): Related location: this proposition could not be proved
 
-Dafny program verifier finished with 9 verified, 1 error
+Dafny program verifier finished with 8 verified, 1 error