changed default decreases clause for functions with a reads clause: use the reads clause followed by the list of parameters

1 files changed, 9 insertions, 10 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 40795129..a6eb404f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3008,18 +3008,17 @@ namespace Microsoft.Dafny {
       List<Expression> decr = f.Decreases.Expressions;

       if (decr.Count == 0) {

         decr = new List<Expression>();

-        if (f.Reads.Count == 0) {

-          foreach (Formal p in f.Formals) {

-            if (IsOrdered(p.Type)) {

-              IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

-              ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

-              decr.Add(ie);  // use the function's first parameter instead

-            }

+        if (f.Reads.Count != 0) {

+          decr.Add(FrameToObjectSet(f.Reads));  // start the lexicographic tuple with the reads clause

+        }

+        foreach (Formal p in f.Formals) {

+          if (IsOrdered(p.Type)) {

+            IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+            ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

+            decr.Add(ie);

           }

-          inferredDecreases = true;

-        } else {

-          decr.Add(FrameToObjectSet(f.Reads));  // use its reads clause instead

         }

+        inferredDecreases = true;  // use 'true' even if decr.Count==0, because this will trigger an error message that asks the user to consider supplying a decreases clause

       }

       return decr;

     }