Fix test-generation translation pass and Update tests

Source/DafnyCore/Verifier/CaptureStateExtensions.cs

@@ -6,7 +6,7 @@ namespace Microsoft.Dafny {
  static class CaptureStateExtensions {
 
  public static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) {
- if (builder.Options.ExpectingModel) {
+ if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
  builder.Add(CaptureState(builder.Options, statement));
  }
  }
@@ -18,7 +18,7 @@ private static Bpl.Cmd CaptureState(DafnyOptions options, Statement stmt) {
  }
 
  public static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) {
- if (builder.Options.ExpectingModel) {
+ if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
  builder.Add(CaptureState(builder.Options, tok, isEndToken, additionalInfo));
  }
  }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect

@@ -3,5 +3,30 @@ git-issue-2026.dfy(18,18): Related message: loop invariant violation
 
 Dafny program verifier finished with 0 verified, 1 error
 Counterexample for first failing assertion: 
+at State git-issue-2026.dfy(12,0): initial state:
  n : int = 2
  ret : _System.array<seq<char>> = ()
+at State git-issue-2026.dfy(13,24):
+ n : int = 2
+ ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+ @0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(15,14):
+ n : int = 2
+ ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+ i : int = 0
+ @0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(16,4): after some loop iterations:
+ n : int = 2
+ ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
+ i : int = 0
+ @0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(22,27):
+ n : int = 2
+ ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+ i : int = 0
+ @0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(26,18):
+ n : int = 2
+ ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+ i : int = 1
+ @0 : seq<char> = ['o', 'd', 'd']

Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect

@@ -3,6 +3,23 @@ counterexample_commandline.dfy(18,22): Related location: this is the postconditi
 
 Dafny program verifier finished with 1 verified, 1 error
 Counterexample for first failing assertion: 
+at State counterexample_commandline.dfy(21,8): initial state:
  this : Patterns.Simple = (p := @0)
  s : seq<char> = ['A']
  @0 : seq<char> = ['?']
+at State counterexample_commandline.dfy(22,22):
+ this : Patterns.Simple = (p := @0)
+ s : seq<char> = ['A']
+ i : int = 0
+ @0 : seq<char> = ['?']
+at State counterexample_commandline.dfy(23,12): after some loop iterations:
+ this : Patterns.Simple = (p := @0)
+ s : seq<char> = ['A']
+ i : int = 0
+ @0 : seq<char> = ['?']
+at State counterexample_commandline.dfy(30,32):
+ this : Patterns.Simple = (p := @0)
+ s : seq<char> = ['A']
+ i : int = 0
+ b : bool = false
+ @0 : seq<char> = ['?']