fix: Fix CanCall assumptions for loop invariants (#1813)

The CanCall assumptions generated at the end of a loop body (to support the expressions in the loop invariant to be proved) were not generated correctly. In particular, when there are multiple invariant declarations, the CanCall assumptions were not given the right antecedents. (See issue #1812 for more details.)

Fixes #1812

Source/Dafny/Verifier/Translator.TrStatement.cs

@@ -1910,12 +1910,15 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr,
         loopBodyBuilder.Add(Bpl.Cmd.SimpleAssign(s.Tok, w, Bpl.Expr.False));
       }
       // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check
-      // of invariant-maintenance can use the appropriate canCall predicates.
-      foreach (AttributedExpression loopInv in s.Invariants) {
-        loopBodyBuilder.Add(TrAssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran)));
+      // of invariant-maintenance can use the appropriate canCall predicates. Note, it is important (see Test/git-issues/git-issue-1812.dfy)
+      // that each CanCall assumption uses the preceding invariants as antecedents--this is achieved by treating all "invariant"
+      // declarations as one big conjunction, because then CanCallAssumption will add the needed antecedents.
+      if (s.Invariants.Any()) {
+        var allInvariants = s.Invariants.Select(inv => inv.E).Aggregate((a, b) => Expression.CreateAnd(a, b));
+        loopBodyBuilder.Add(TrAssumeCmd(s.Tok, CanCallAssumption(allInvariants, etran)));
       }
-      Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok);
 
+      Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok);
       builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, body));
     }
     void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,

Test/git-issues/git-issue-1812.dfy

@@ -0,0 +1,37 @@
+// RUN: %dafny "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function Max(s: set<int>): (m: int)
+  requires s != {}
+{
+  var x :| x in s;
+  if s == {x} then
+    x
+  else
+    var s' := s - {x};
+    var y := Max(s');
+    y
+}
+
+method IncorrectLoop0(m: int)
+{
+  var r := {m};
+  while r != {}
+    // Incorrectly generated CanCall assumptions for multiple invariant declarations
+    // once caused the error on the next line to be omitted.
+    invariant r != {} // error: loop invariant not maintained
+    invariant m == Max(r)
+  {
+    r := r - {m};
+  }
+}
+
+method IncorrectLoop1(m: int)
+{
+  var r := {m};
+  while r != {}
+    invariant r != {} && m == Max(r) // error: loop invariant not maintained
+  {
+    r := r - {m};
+  }
+}

Test/git-issues/git-issue-1812.dfy.expect

@@ -0,0 +1,6 @@
+git-issue-1812.dfy(22,16): Error: This loop invariant might not be maintained by the loop.
+git-issue-1812.dfy(22,16): Related message: loop invariant violation
+git-issue-1812.dfy(33,16): Error: This loop invariant might not be maintained by the loop.
+git-issue-1812.dfy(33,16): Related message: loop invariant violation
+
+Dafny program verifier finished with 1 verified, 2 errors