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