From acaaff08eeceacb6f92492029d9caa744a8d4a2c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 8 Apr 2022 15:33:12 -0500 Subject: [PATCH] Fixed the test provenance --- Test/git-issues/git-issue-1604b2.dfy.expect | 26 +++++++-------- Test/git-issues/git-issue-1604e.dfy.expect | 26 +++++++-------- Test/git-issues/git-issue-1604g.dfy.expect | 36 ++++++++++----------- 3 files changed, 44 insertions(+), 44 deletions(-) diff --git a/Test/git-issues/git-issue-1604b2.dfy.expect b/Test/git-issues/git-issue-1604b2.dfy.expect index 0c0a1827f2b..f133d980bb7 100644 --- a/Test/git-issues/git-issue-1604b2.dfy.expect +++ b/Test/git-issues/git-issue-1604b2.dfy.expect @@ -1,15 +1,15 @@ -git-issue-1604e.dfy(65,37): Error: Could not prove that the range constrains the bound variable 'go' to be of type GhostOrdinalCell, and since GhostOrdinalCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. -git-issue-1604e.dfy(24,24): [Related location] The subset type GhostOrdinalCelltype GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell -git-issue-1604e.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604e.dfy(65,103): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell' -git-issue-1604e.dfy(67,37): Error: Could not prove that the range constrains the bound variable 'go2' to be of type GhostOrdinalCell2, and since GhostOrdinalCell2 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type CompilableNaturalCell. -git-issue-1604e.dfy(26,55): [Related location] GhostOrdinalCell2 is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604e.dfy(67,37): Error: value does not satisfy the subset constraints of 'set' -git-issue-1604e.dfy(67,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell' -git-issue-1604e.dfy(69,37): Error: Could not prove that the range constrains the bound variable 'go3' to be of type GhostOrdinalCell3, and since GhostOrdinalCell3 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. -git-issue-1604e.dfy(28,25): [Related location] The subset type GhostOrdinalCell3type GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell -git-issue-1604e.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604e.dfy(69,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell' -git-issue-1604e.dfy(71,9): Error: assertion might not hold +git-issue-1604b2.dfy(65,37): Error: Could not prove that the range constrains the bound variable 'go' to be of type GhostOrdinalCell, and since GhostOrdinalCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. +git-issue-1604b2.dfy(24,24): [Related location] The subset type GhostOrdinalCelltype GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell +git-issue-1604b2.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604b2.dfy(65,103): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell' +git-issue-1604b2.dfy(67,37): Error: Could not prove that the range constrains the bound variable 'go2' to be of type GhostOrdinalCell2, and since GhostOrdinalCell2 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type CompilableNaturalCell. +git-issue-1604b2.dfy(26,55): [Related location] GhostOrdinalCell2 is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604b2.dfy(67,37): Error: value does not satisfy the subset constraints of 'set' +git-issue-1604b2.dfy(67,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell' +git-issue-1604b2.dfy(69,37): Error: Could not prove that the range constrains the bound variable 'go3' to be of type GhostOrdinalCell3, and since GhostOrdinalCell3 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. +git-issue-1604b2.dfy(28,25): [Related location] The subset type GhostOrdinalCell3type GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell +git-issue-1604b2.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604b2.dfy(69,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell' +git-issue-1604b2.dfy(71,9): Error: assertion might not hold Dafny program verifier finished with 12 verified, 8 errors diff --git a/Test/git-issues/git-issue-1604e.dfy.expect b/Test/git-issues/git-issue-1604e.dfy.expect index fe6c108164b..f43e9b13e63 100644 --- a/Test/git-issues/git-issue-1604e.dfy.expect +++ b/Test/git-issues/git-issue-1604e.dfy.expect @@ -1,15 +1,15 @@ -git-issue-1604b.dfy(54,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. -git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604b.dfy(54,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell' -git-issue-1604b.dfy(57,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. -git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604b.dfy(60,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. -git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604b.dfy(63,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell' -git-issue-1604b.dfy(66,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. -git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604b.dfy(66,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell' -git-issue-1604b.dfy(69,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell' -git-issue-1604b.dfy(71,9): Error: assertion might not hold +git-issue-1604e.dfy(54,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. +git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604e.dfy(54,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell' +git-issue-1604e.dfy(57,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. +git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604e.dfy(60,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. +git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604e.dfy(63,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell' +git-issue-1604e.dfy(66,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell. +git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604e.dfy(66,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell' +git-issue-1604e.dfy(69,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell' +git-issue-1604e.dfy(71,9): Error: assertion might not hold Dafny program verifier finished with 9 verified, 9 errors diff --git a/Test/git-issues/git-issue-1604g.dfy.expect b/Test/git-issues/git-issue-1604g.dfy.expect index 5dbb4e166ef..64f748c8886 100644 --- a/Test/git-issues/git-issue-1604g.dfy.expect +++ b/Test/git-issues/git-issue-1604g.dfy.expect @@ -1,20 +1,20 @@ -git-issue-1604f.dfy(38,8): Error: Could not prove that the range constrains the bound variable 'f' to be of type SpecialFruit, and since SpecialFruit is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Fruit. -git-issue-1604f.dfy(16,31): [Related location] SpecialFruit is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -git-issue-1604f.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time -git-issue-1604f.dfy(19,11): Related location -git-issue-1604f.dfy(13,2): Related location -git-issue-1604f.dfy(8,25): Related location -git-issue-1604f.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time -git-issue-1604f.dfy(19,11): Related location -git-issue-1604f.dfy(13,2): Related location -git-issue-1604f.dfy(9,19): Related location -git-issue-1604f.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time -git-issue-1604f.dfy(19,11): Related location -git-issue-1604f.dfy(13,2): Related location -git-issue-1604f.dfy(8,25): Related location -git-issue-1604f.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time -git-issue-1604f.dfy(19,11): Related location -git-issue-1604f.dfy(13,2): Related location -git-issue-1604f.dfy(9,19): Related location +git-issue-1604g.dfy(38,8): Error: Could not prove that the range constrains the bound variable 'f' to be of type SpecialFruit, and since SpecialFruit is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Fruit. +git-issue-1604g.dfy(16,31): [Related location] SpecialFruit is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +git-issue-1604g.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time +git-issue-1604g.dfy(19,11): Related location +git-issue-1604g.dfy(13,2): Related location +git-issue-1604g.dfy(8,25): Related location +git-issue-1604g.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time +git-issue-1604g.dfy(19,11): Related location +git-issue-1604g.dfy(13,2): Related location +git-issue-1604g.dfy(9,19): Related location +git-issue-1604g.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time +git-issue-1604g.dfy(19,11): Related location +git-issue-1604g.dfy(13,2): Related location +git-issue-1604g.dfy(8,25): Related location +git-issue-1604g.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time +git-issue-1604g.dfy(19,11): Related location +git-issue-1604g.dfy(13,2): Related location +git-issue-1604g.dfy(9,19): Related location Dafny program verifier finished with 4 verified, 5 errors