adjust ids again

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect

@@ -1,5 +1,4 @@
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined.
 TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined.
-TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined.
 
 Dafny program verifier finished with 0 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect

@@ -7,7 +7,7 @@ Processing call to procedure bar (call precondtion) in implementation foo (corre
 Processing call to procedure bar (call postcondition) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)):
   >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && $Unbox(read(call0old#AT#$Heap, $o, alloc)): bool ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap)))
   >>> added after: a##cached##1 := a##cached##1 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
-Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id8"} Lit(false);
+Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id7"} Lit(false);
   >>> MarkAsPartiallyVerified
 Snapshots0.v1.dfy(4,9): Error: assertion might not hold
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect

@@ -4,7 +4,7 @@ Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id2"} Lit(false);
 Dafny program verifier finished with 1 verified, 0 errors
 Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)):
   >>> added after: a##cached##0 := a##cached##0 && false;
-Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id9"} Lit(false);
+Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id8"} Lit(false);
   >>> DoNothingToAssert
 Snapshots1.v1.dfy(4,9): Error: assertion might not hold
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect

@@ -1,12 +1,12 @@
 Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id2"} Lit(false);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id7"} Lit(true);
+Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id6"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id6"} _module.__default.P() <==> _module.__default.Q();
+Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id5"} _module.__default.P() <==> _module.__default.Q();
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id10"} Lit(true);
+Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id9"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id9"} _module.__default.Q() <==> Lit(_module.__default.R());
+Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id8"} _module.__default.Q() <==> Lit(_module.__default.R());
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 3 verified, 0 errors
@@ -16,16 +16,16 @@ Processing implementation P (well-formedness) (at Snapshots2.v1.dfy(10,11)):
   >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
 Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)):
   >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
-Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id15"} Lit(false);
+Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id14"} Lit(false);
   >>> DoNothingToAssert
 Snapshots2.v1.dfy(4,9): Error: assertion might not hold
-Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id20"} Lit(true);
+Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id18"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id19"} _module.__default.P() <==> _module.__default.Q();
+Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id17"} _module.__default.P() <==> _module.__default.Q();
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id23"} Lit(true);
+Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id21"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id22"} _module.__default.Q() <==> Lit(_module.__default.R());
+Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id20"} _module.__default.Q() <==> Lit(_module.__default.R());
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 2 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect

@@ -15,13 +15,13 @@ Snapshots5.v1.dfy(13,10): Warning: Could not find a trigger for this quantifier.
 Snapshots5.v1.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 Snapshots5.v1.dfy(22,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 Snapshots5.v1.dfy(27,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id14"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0;
+Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id13"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id17"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3;
+Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id16"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id18"} (exists b#3_1: bool :: Lit(true)) || 4 != 4;
+Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id17"} (exists b#3_1: bool :: Lit(true)) || 4 != 4;
   >>> DoNothingToAssert
-Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id19"} (exists b#3: bool :: Lit(true)) || 5 != 5;
+Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id18"} (exists b#3: bool :: Lit(true)) || 5 != 5;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect

@@ -8,35 +8,35 @@ Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id5$id2$requires"} {
 Snapshots8.v0.dfy(3,11): Error: assertion might not hold
 Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved
 Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved
-Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id11"} LitInt(2) <= z#0;
+Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id9"} LitInt(2) <= z#0;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path
 Snapshots8.v0.dfy(13,12): Related location: this is the postcondition that could not be proved
-Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id13"} u#0 != 53;
+Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id11"} u#0 != 53;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(23,11): Error: assertion might not hold
-Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id14"} Lit(true);
+Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id12"} Lit(true);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 4 errors
-Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id30"} u#0 != 53;
+Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id26"} u#0 != 53;
   >>> RecycleError
 Snapshots8.v1.dfy(30,16): Error: assertion might not hold
-Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id15"} x#0 < 20 || LitInt(10) <= x#0;
+Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id13"} x#0 < 20 || LitInt(10) <= x#0;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id16"} x#0 < 10;
+Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id14"} x#0 < 10;
   >>> RecycleError
-Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id21$id17$requires"} {:id "id17"} LitInt(0) <= call0formal#AT#y#0;
+Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id19$id15$requires"} {:id "id15"} LitInt(0) <= call0formal#AT#y#0;
   >>> RecycleError
-Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id19"} x#0 == LitInt(7);
+Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id17"} x#0 == LitInt(7);
   >>> DoNothingToAssert
 Snapshots8.v1.dfy(5,16): Error: assertion might not hold
 Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved
 Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved
 Snapshots8.v1.dfy(7,11): Error: assertion might not hold
-Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id29"} Lit(true);
+Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id25"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id27"} LitInt(2) <= z#0;
+Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id23"} LitInt(2) <= z#0;
   >>> DoNothingToAssert
 Snapshots8.v1.dfy(24,9): Error: a postcondition could not be proved on this return path
 Snapshots8.v1.dfy(19,12): Related location: this is the postcondition that could not be proved

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect

@@ -1,19 +1,19 @@
 Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
-Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id3"} ok#0;
+Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0;
   >>> DoNothingToAssert
 Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path
 Snapshots9.v0.dfy(2,10): Related location: this is the postcondition that could not be proved
-Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id9"} ok#0;
+Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id7"} ok#0;
   >>> DoNothingToAssert
 Snapshots9.v0.dfy(13,0): Error: a postcondition could not be proved on this return path
 Snapshots9.v0.dfy(12,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id13"} ok#0;
+Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id10"} ok#0;
   >>> RecycleError
 Snapshots9.v1.dfy(8,7): Error: a postcondition could not be proved on this return path
 Snapshots9.v1.dfy(6,10): Related location: this is the postcondition that could not be proved
-Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id19"} ok#0;
+Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id15"} ok#0;
   >>> RecycleError
 Snapshots9.v1.dfy(21,0): Error: a postcondition could not be proved on this return path
 Snapshots9.v1.dfy(19,10): Related location: this is the postcondition that could not be proved

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

@@ -1,10 +1,10 @@
-git-issue-3855.dfy(801,0): Warning: attribute :ignore is deprecated
-git-issue-3855.dfy(801,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
-git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved
+git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated
+git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
+git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved
-git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved
+git-issue-3855.dfy(942,17): 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
-git-issue-3855.dfy(1337,20): Error: a precondition for this call could not be proved
+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

Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect

@@ -3,7 +3,5 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are
 triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined.
 triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined.
 triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined.
-triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined.
-triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined.
 
 Dafny program verifier finished with 1 verified, 0 errors