Enable isolating all return statements

Source/DafnyCore/AST/Tokens.cs

@@ -66,6 +66,7 @@ public Token(int linenum, int colnum) {
     this.val = "";
   }
 
+  public bool IsSourceToken => this != NoToken;
   public int kind { get; set; } // Used by coco, so we can't rename it to Kind
 
   public string ActualFilename => Filepath;
@@ -160,6 +161,8 @@ public bool IsValid {
     get { return WrappedToken.IsValid; }
   }
 
+  public virtual bool IsSourceToken => false;
+
   public int kind {
     get { return WrappedToken.kind; }
     set { WrappedToken.kind = value; }
@@ -305,6 +308,8 @@ public override IToken WithVal(string newVal) {
     throw new NotImplementedException();
   }
 
+  public override bool IsSourceToken => this != NoToken;
+
   public BoogieRangeToken ToToken() {
     return new BoogieRangeToken(StartToken, EndToken, null);
   }

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.4.1" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.4.2" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyDriver/CliCompilation.cs

@@ -198,7 +198,7 @@ string OriginDescription(IImplementationPartOrigin origin, bool outer) {
             var result = origin switch {
               PathOrigin pathOrigin => $"{OriginDescription(pathOrigin.Inner, false)}" +
                                        $"after executing lines {string.Join(", ", pathOrigin.BranchTokens.Select(b => b.line))}",
-              RemainingAssertionsOrigin remainingAssertions => $"{OriginDescription(remainingAssertions.Origin, false)}remaining assertions",
+              RemainingAssertionsOrigin remainingAssertions => OriginDescription(remainingAssertions.Origin, false) + (outer ? "remaining assertions" : ""),
               IsolatedAssertionOrigin isolateOrigin => $"{OriginDescription(isolateOrigin.Origin, false)}assertion at line {isolateOrigin.line}",
               JumpOrigin returnOrigin => $"{OriginDescription(returnOrigin.Origin, false)}{JumpOriginKind(returnOrigin)} at line {returnOrigin.line}",
               AfterSplitOrigin splitOrigin => $"{OriginDescription(splitOrigin.Inner, false)}assertions after split_here at line {splitOrigin.line}",

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy

@@ -1,9 +1,9 @@
 // RUN: ! %verify --isolate-assertions --cores=1 --progress VerificationJobs "%s" &> %t.raw
 // RUN: %sed 's#\(time.*\)#<redacted>#g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
-
-ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)}
-
+ghost function f(i:nat, j:nat):int {
+  if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)
+}
 lemma{:resource_limit 10000000} L()
 {
   assert true;

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy

@@ -1,13 +1,19 @@
-// RUN: %verify --progress VerificationJobs --cores=1 %s &> %t.raw
+// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t.raw
 // RUN: %sed 's#\(time.*\)#<redacted>#g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
 
 
-
-
-method {:isolate_assertions} Foo() {
+method {:isolate_assertions} Foo(x: int) returns (r: int) 
+  ensures r > 3
+  ensures r < 10 
+{
   assert true;
   assert true;
+  if (x == 3) {
+    return 7;
+  } else {
+    return 12;
+  }
 }
 
 method Bar() {

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect

@@ -1,7 +1,13 @@
 Verified 0/2 symbols. Waiting for Foo to verify.
-Verified 1/2 of Foo: assertion at line 9 - verified successfully <redacted>
-Verified 2/2 of Foo: assertion at line 10 - verified successfully <redacted>
+Verified 1/6 of Foo: assertion at line 10 - verified successfully <redacted>
+Verified 2/6 of Foo: assertion at line 11 - verified successfully <redacted>
+Verified 3/6 of Foo: return at line 15, assertion at line 7 - verified successfully <redacted>
+Verified 4/6 of Foo: return at line 15, assertion at line 8 - could not be verified <redacted>
+Verified 5/6 of Foo: return at line 13, assertion at line 7 - verified successfully <redacted>
+Verified 6/6 of Foo: return at line 13, assertion at line 8 - verified successfully <redacted>
+isolateAllAssertions.dfy(15,4): Error: a postcondition could not be proved on this return path
+isolateAllAssertions.dfy(8,12): Related location: this is the postcondition that could not be proved
 Verified 1/2 symbols. Waiting for Bar to verify.
 Verified 1/1 of Bar: entire body - verified successfully <redacted>
 
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 6 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect

@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 142 verified, 0 errors
+Dafny program verifier finished with 148 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect

@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 55 verified, 0 errors
+Dafny program verifier finished with 67 verified, 0 errors

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.4.1" />
+-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.4.2" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />

docs/dev/news/5917.feat

@@ -0,0 +1 @@
+When using `--isolate-assertions` or `{:isolate_assertions}`, a separate assertion batch will be generated per pair of return statement and ensures clause.