Fix variable printing order and update tests

Source/DafnyDriver/CompilerDriver.cs

@@ -356,7 +356,7 @@ private static void PrintCounterexample(DafnyOptions options) {
  var model = new DafnyModel(firstCounterexample.Model, options);
  options.OutputWriter.WriteLine("Counterexample for first failing assertion: ");
  foreach (var state in model.States.Where(state => state.StateContainsPosition())) {
- options.OutputWriter.WriteLine($"at State {state.FullStateName}:");
+ options.OutputWriter.WriteLine(state.FullStateName + ":");
  var vars = state.ExpandedVariableSet(-1);
  foreach (var variable in vars) {
  options.OutputWriter.WriteLine($"\t{variable.ShortName} : " +

Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs

@@ -56,8 +56,8 @@ internal DafnyModelState(DafnyModel model, Model.CapturedState state) {
  /// <param name="maxDepth">The maximum depth up to which to expand the
  /// variable set.</param>
  /// <returns>Set of variables</returns>
- public HashSet<DafnyModelVariable> ExpandedVariableSet(int maxDepth) {
- HashSet<DafnyModelVariable> expandedSet = new();
+ public List<DafnyModelVariable> ExpandedVariableSet(int maxDepth) {
+ List<DafnyModelVariable> expandedSet = new();
  // The following is the queue for elements to be added to the set. The 2nd
  // element of a tuple is the depth of the variable w.r.t. the original set
  List<Tuple<DafnyModelVariable, int>> varsToAdd = new();

Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs

@@ -106,7 +106,7 @@ private IEnumerable<CounterExampleItem> GetCounterExamples(DafnyModel model) {
  }
 
  private CounterExampleItem GetCounterExample(DafnyModelState state) {
- HashSet<DafnyModelVariable> vars = state.ExpandedVariableSet(counterExampleDepth);
+ List<DafnyModelVariable> vars = state.ExpandedVariableSet(counterExampleDepth);
  return new(
  new Position(state.GetLineId() - 1, state.GetCharId()),
  vars.WithCancellation(cancellationToken).ToDictionary(

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

@@ -3,29 +3,29 @@ 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:
+git-issue-2026.dfy(12,0): initial state:
  n : int = 2
  ret : _System.array<seq<char>> = ()
-at State git-issue-2026.dfy(13,24):
+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):
+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:
+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):
+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):
+git-issue-2026.dfy(26,18):
  n : int = 2
  ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
  i : int = 1

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

@@ -3,21 +3,21 @@ 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:
+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):
+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:
+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):
+counterexample_commandline.dfy(30,32):
  this : Patterns.Simple = (p := @0)
  s : seq<char> = ['A']
  i : int = 0