fix tests

dafny-lang · Oct 15, 2024 · da63cb5 · da63cb5
1 parent 915bbcf
commit da63cb5
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect
@@ -4,7 +4,7 @@ Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id1"} Lit(false);
 Dafny program verifier finished with 1 verified, 0 errors
 Processing call to procedure N (call) 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 "id6"} 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
 

diff --git a/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect
@@ -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 "id12"} 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 "id16"} 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 "id15"} _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 "id19"} 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 "id18"} _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
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect
@@ -7,4 +7,4 @@ ProofRefactorings.dfy(92,11): Info: This requires clause was only used to prove
 ProofRefactorings.dfy(99,0): Info: Consider hiding this function, which is unused by the proof: P
 ProofRefactorings.dfy(107,9): Info: This fact was only used to prove the assertion ProofRefactorings.dfy(109,10)-(109,10). Consider moving it into a by-proof.
 
-Dafny program verifier finished with 44 verified, 0 errors
+Dafny program verifier finished with 22 verified, 0 errors