Dafny: For functions with an empty decreases clause that use the reads clause instead, do not include wildcards.

1 files changed, 6 insertions, 1 deletions

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 092ee146..35e8cdc1 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1435,7 +1435,12 @@ namespace Microsoft.Dafny {
     List<Expression!>! ProjectOutSpecificFields(List<FrameExpression!>! fexprs) {

       List<Expression!> exprs = new List<Expression!>();

       foreach (FrameExpression fe in fexprs) {

-        exprs.Add(fe.E);

+        if (fe.E is WildcardExpr) {

+          // drop wildcards altogether

+        } else {

+          // keep only fe.E, drop any fe.Field designation

+          exprs.Add(fe.E);

+        }

       }

       return exprs;

     }