Resolve attributes of a forall statement only after bound variables have been added to the scope.

Resolve the attributes of local variables.
Don't resolve attributes of PredicateStmt's more than once.

1 files changed, 15 insertions, 15 deletions

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 87cc4a84..824ad991 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -94,14 +94,14 @@ SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decrease
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(681,14): Error: assertion violation

+SmallTests.dfy(690,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(678,5): anon7_LoopHead

+    SmallTests.dfy(687,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(678,5): anon8_Else

+    SmallTests.dfy(687,5): anon8_Else

     (0,0): anon9_Then

-SmallTests.dfy(702,14): Error: assertion violation

+SmallTests.dfy(711,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

@@ -133,12 +133,12 @@ SmallTests.dfy(400,41): Related location: This is the postcondition that might n
 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-SmallTests.dfy(552,12): Error: assertion violation

+SmallTests.dfy(561,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-SmallTests.dfy(566,20): Error: left-hand sides 0 and 1 may refer to the same location

+SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -150,11 +150,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-SmallTests.dfy(568,15): Error: left-hand sides 1 and 2 may refer to the same location

+SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    SmallTests.dfy(561,18): anon28_Else

+    SmallTests.dfy(570,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon30_Then

@@ -165,16 +165,16 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(575,25): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(588,10): Error: assertion violation

+SmallTests.dfy(597,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(612,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(635,10): Error: assertion violation

+SmallTests.dfy(644,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -182,17 +182,17 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-SmallTests.dfy(649,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(658,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

     (0,0): anon3

-SmallTests.dfy(651,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(660,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-SmallTests.dfy(664,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(673,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0