From d731efa64234015f6f785c31988bbc9314f0b51b Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Fri, 2 Sep 2022 03:05:08 -0700
Subject: [PATCH] feat: Generate a warning when 'old' has no effect (#2610)

Fixes #1989

If the argument to `old` has no dereferences of the mutable heap, generate a warning saying that the `old` has no effect. This has been a common source of errors and confusion.
---
 RELEASE_NOTES.md                              |   2 +-
 Source/Dafny/AST/DafnyAst.cs                  |  20 +-
 Source/Dafny/AST/FreeVariablesUtil.cs         |  18 +-
 Source/Dafny/Resolver.cs                      |  16 +-
 Source/Dafny/Rewriter.cs                      |  10 +
 Source/Dafny/Triggers/TriggerUtils.cs         |   2 +-
 Source/Dafny/UselessOldLinter.cs              |  51 ++++
 Source/Dafny/Verifier/Translator.cs           |   6 +-
 Test/VSComp2010/Problem4-Queens.dfy           |   1 -
 Test/allocated1/dafny0/Simple.dfy.expect      |   1 +
 Test/allocated1/dafny0/SmallTests.dfy.expect  |   2 +
 .../dafny0/Twostate-Verification.dfy.expect   |   1 +
 Test/concurrency/12-MutexLifetime-long.dfy    |   7 +-
 Test/concurrency/12-MutexLifetime-short.dfy   |   7 +-
 .../12-MutexLifetime-short.dfy.expect         |   2 +-
 Test/dafny0/LabeledAsserts.dfy.expect         |   2 +
 Test/dafny0/LabelsOldAt.dfy.expect            |   1 +
 Test/dafny0/OpaqueTypeWithMembers.dfy         |   6 +-
 Test/dafny0/OpaqueTypeWithMembers.dfy.expect  |   3 +
 Test/dafny0/Simple.dfy                        |   2 +-
 Test/dafny0/Simple.dfy.expect                 |   1 +
 Test/dafny0/SmallTests.dfy.expect             |   2 +
 Test/dafny0/Twostate-Verification.dfy         |  46 ++--
 Test/dafny0/Twostate-Verification.dfy.expect  |  23 ++
 Test/dafny0/TypeMembers.dfy                   |   2 +-
 Test/dafny0/TypeMembers.dfy.expect            |   1 +
 Test/git-issues/git-issue-1163.dfy            |   2 +-
 Test/git-issues/git-issue-1163.dfy.expect     |   1 +
 Test/git-issues/git-issue-1989.dfy            | 238 ++++++++++++++++++
 Test/git-issues/git-issue-1989.dfy.expect     |  31 +++
 Test/refman/Example-Old.dfy.expect            |   3 +
 Test/refman/Example-Old3.dfy.expect           |   1 +
 Test/traits/TraitOverride2.dfy                |   4 -
 Test/traits/TraitOverride2.dfy.expect         |   2 +-
 ...ping-is-hard-to-decide-modulo-equality.dfy |   2 +-
 .../old-is-a-special-case-for-triggers.dfy    |  29 ++-
 ...-is-a-special-case-for-triggers.dfy.expect |  30 ++-
 37 files changed, 508 insertions(+), 70 deletions(-)
 create mode 100644 Source/Dafny/UselessOldLinter.cs
 create mode 100644 Test/git-issues/git-issue-1989.dfy
 create mode 100644 Test/git-issues/git-issue-1989.dfy.expect

diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index d6bbcea573d..a5a276b6120 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -2,6 +2,7 @@
 
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
+- feat: generate warning when 'old' has no effect
 
 # 3.8.1
 
@@ -15,7 +16,6 @@
 - fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
 - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)
 
-
 # 3.8.0
 
 - fix: Use the right bitvector comparison in decrease checks
diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs
index 7a609536d6c..14aee1ffdc1 100644
--- a/Source/Dafny/AST/DafnyAst.cs
+++ b/Source/Dafny/AST/DafnyAst.cs
@@ -6723,6 +6723,24 @@ public Statement(IToken tok, IToken endTok)
       Contract.Requires(endTok != null);
     }
 
+    /// <summary>
+    /// Returns the non-null expressions of this statement proper (that is, do not include the expressions of substatements).
+    /// Filters all sub expressions that are not part of specifications
+    /// </summary>
+    public IEnumerable<Expression> SubExpressionsIncludingTransitiveSubStatements {
+      get {
+        foreach (var e in SubExpressions) {
+          yield return e;
+        }
+
+        foreach (var s in SubStatements) {
+          foreach (var e in s.SubExpressionsIncludingTransitiveSubStatements) {
+            yield return e;
+          }
+        }
+      }
+    }
+
     /// <summary>
     /// Returns the non-null substatements of the Statements.
     /// </summary>
@@ -8759,7 +8777,7 @@ public TryRecoverStatement(Statement tryBody, IVariable haltMessageVar, Statemen
   // ------------------------------------------------------------------------------------------------------
 
   public abstract class TokenWrapper : IToken {
-    protected readonly IToken WrappedToken;
+    public readonly IToken WrappedToken;
     protected TokenWrapper(IToken wrappedToken) {
       Contract.Requires(wrappedToken != null);
       WrappedToken = wrappedToken;
diff --git a/Source/Dafny/AST/FreeVariablesUtil.cs b/Source/Dafny/AST/FreeVariablesUtil.cs
index bc0a4ef9229..6f8fd670124 100644
--- a/Source/Dafny/AST/FreeVariablesUtil.cs
+++ b/Source/Dafny/AST/FreeVariablesUtil.cs
@@ -35,17 +35,20 @@ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs) {
       bool dontCare0 = false, dontCare1 = false;
       Type dontCareT = null;
       var dontCareHeapAt = new HashSet<Label>();
-      ComputeFreeVariables(expr, fvs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref dontCareT);
+      ComputeFreeVariables(expr, fvs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref dontCareT, false);
     }
-    public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap) {
+    public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, bool includeStatements = false) {
       Contract.Requires(expr != null);
       Contract.Requires(fvs != null);
       bool dontCare1 = false;
       Type dontCareT = null;
       var dontCareHeapAt = new HashSet<Label>();
-      ComputeFreeVariables(expr, fvs, ref usesHeap, ref dontCare1, dontCareHeapAt, ref dontCareT);
+      ComputeFreeVariables(expr, fvs, ref usesHeap, ref dontCare1, dontCareHeapAt, ref dontCareT, includeStatements);
     }
-    public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, ref bool usesOldHeap, ISet<Label> freeHeapAtVariables, ref Type usesThis) {
+    public static void ComputeFreeVariables(Expression expr,
+      ISet<IVariable> fvs,
+      ref bool usesHeap, ref bool usesOldHeap, ISet<Label> freeHeapAtVariables, ref Type usesThis,
+      bool includeStatements) {
       Contract.Requires(expr != null);
 
       if (expr is ThisExpr) {
@@ -113,8 +116,13 @@ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, re
       // visit subexpressions
       bool uHeap = false, uOldHeap = false;
       Type uThis = null;
+      if (expr is StmtExpr stmtExpr && includeStatements) {
+        foreach (var subExpression in stmtExpr.S.SubExpressionsIncludingTransitiveSubStatements) {
+          ComputeFreeVariables(subExpression, fvs, ref uHeap, ref uOldHeap, freeHeapAtVariables, ref uThis, includeStatements);
+        }
+      }
       foreach (var subExpression in expr.SubExpressions) {
-        ComputeFreeVariables(subExpression, fvs, ref uHeap, ref uOldHeap, freeHeapAtVariables, ref uThis);
+        ComputeFreeVariables(subExpression, fvs, ref uHeap, ref uOldHeap, freeHeapAtVariables, ref uThis, includeStatements);
       }
       Contract.Assert(usesThis == null || uThis == null || usesThis.Equals(uThis));
       usesThis = usesThis ?? uThis;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d2eac9eb3ba..b3f95e3f6fa 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -441,6 +441,8 @@ public void ResolveProgram(Program prog) {
         rewriters.Add(new ConstructorWarning(reporter));
       }
 
+      rewriters.Add(new UselessOldLinter(reporter));
+
       foreach (var plugin in DafnyOptions.O.Plugins) {
         rewriters.AddRange(plugin.GetRewriters(reporter));
       }
@@ -10622,6 +10624,8 @@ void ResolveIterator(IteratorDecl iter) {
     void CreateIteratorMethodSpecs(IteratorDecl iter) {
       Contract.Requires(iter != null);
 
+      var tok = new AutoGeneratedToken(iter.tok);
+
       // ---------- here comes the constructor ----------
       // same requires clause as the iterator itself
       iter.Member_Init.Req.AddRange(iter.Requires);
@@ -10653,7 +10657,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
       }
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
         new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"),
-        new OldExpr(iter.tok, frameSet))));
+        new OldExpr(tok, frameSet))));
       // ensures this._modifies == old(ModifiesClause);
       modSetSingletons = new List<Expression>();
       frameSet = new SetDisplayExpr(iter.tok, true, modSetSingletons);
@@ -10668,7 +10672,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
       }
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
         new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"),
-        new OldExpr(iter.tok, frameSet))));
+        new OldExpr(tok, frameSet))));
       // ensures this._new == {};
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
         new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
@@ -10679,7 +10683,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
         var p = iter.Decreases.Expressions[i];
         ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
           new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name),
-          new OldExpr(iter.tok, p))));
+          new OldExpr(tok, p))));
       }
 
       // ---------- here comes predicate Valid() ----------
@@ -10705,7 +10709,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
       ens.Add(new AttributedExpression(new FreshExpr(iter.tok,
         new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub,
           new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
-          new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
+          new OldExpr(tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
       // ensures null !in _new
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.NotIn,
         new LiteralExpr(iter.tok),
@@ -10722,9 +10726,9 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
         var ys = iter.OutsHistoryFields[i];
         var ite = new ITEExpr(iter.tok, false, new IdentifierExpr(iter.tok, "more"),
           new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add,
-            new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),
+            new OldExpr(tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),
             new SeqDisplayExpr(iter.tok, new List<Expression>() { new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), y.Name) })),
-          new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)));
+          new OldExpr(tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)));
         var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite);
         ens.Add(new AttributedExpression(eq));
       }
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index bb8d57fd627..ba0c6c43051 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -122,6 +122,16 @@ public AutoGeneratedToken(IToken wrappedToken)
       : base(wrappedToken) {
       Contract.Requires(wrappedToken != null);
     }
+
+    public static bool Is(IToken tok) {
+      while (tok is TokenWrapper w) {
+        if (w is AutoGeneratedToken) {
+          return true;
+        }
+        tok = w.WrappedToken;
+      }
+      return false;
+    }
   }
 
   public class TriggerGeneratingRewriter : IRewriter {
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index eb4898378f1..6f0c6f21c2c 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -286,7 +286,7 @@ internal static IEnumerable<Expression> MaybeWrapInOld(Expression expr, HashSet<
       Contract.Requires(wrap == null || wrap.Count != 0);
       if (wrap != null && !(expr is NameSegment) && !(expr is IdentifierExpr)) {
         foreach (var w in wrap) {
-          var newExpr = new OldExpr(expr.tok, expr, w.At) { AtLabel = w.AtLabel };
+          var newExpr = new OldExpr(new AutoGeneratedToken(expr.tok), expr, w.At) { AtLabel = w.AtLabel };
           newExpr.Type = expr.Type;
           yield return newExpr;
         }
diff --git a/Source/Dafny/UselessOldLinter.cs b/Source/Dafny/UselessOldLinter.cs
new file mode 100644
index 00000000000..3b509d66c33
--- /dev/null
+++ b/Source/Dafny/UselessOldLinter.cs
@@ -0,0 +1,51 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+//
+//-----------------------------------------------------------------------------
+using System.Collections.Generic;
+using System.Linq;
+using System.Reactive;
+
+namespace Microsoft.Dafny {
+
+  public class UselessOldLinter : IRewriter {
+    internal override void PostResolve(Program program) {
+      base.PostResolve(program);
+      foreach (var moduleDefinition in program.Modules()) {
+        foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+          foreach (var callable in topLevelDecl.Members.OfType<ICallable>()) {
+            var visitor = new UselessOldLinterVisitor(this.Reporter);
+            visitor.Visit(callable, Unit.Default);
+          }
+        }
+      }
+    }
+
+    public UselessOldLinter(ErrorReporter reporter) : base(reporter) {
+    }
+  }
+
+  class UselessOldLinterVisitor : TopDownVisitor<Unit> {
+    private readonly ErrorReporter reporter;
+
+    public UselessOldLinterVisitor(ErrorReporter reporter) {
+      this.reporter = reporter;
+    }
+
+    protected override bool VisitOneExpr(Expression expr, ref Unit st) {
+      if (expr is OldExpr oldExpr && !AutoGeneratedToken.Is(oldExpr.tok)) {
+        var fvs = new HashSet<IVariable>();
+        var usesHeap = false;
+        FreeVariablesUtil.ComputeFreeVariables(oldExpr.E, fvs, ref usesHeap, true);
+        if (!usesHeap) {
+          this.reporter.Warning(MessageSource.Rewriter, oldExpr.tok,
+            $"Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect");
+        }
+      }
+      return base.VisitOneExpr(expr, ref st);
+    }
+  }
+}
diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs
index dc22ffbeb15..f324f8cfa80 100644
--- a/Source/Dafny/Verifier/Translator.cs
+++ b/Source/Dafny/Verifier/Translator.cs
@@ -1968,7 +1968,7 @@ void AddFunctionAxiom(Bpl.Function boogieFunction, Function f, Expression body)
         bool dontCare0 = false, dontCare1 = false;
         var dontCareHeapAt = new HashSet<Label>();
         foreach (var e in f.Decreases.Expressions) {
-          FreeVariablesUtil.ComputeFreeVariables(e, FVs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref usesThis);
+          FreeVariablesUtil.ComputeFreeVariables(e, FVs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref usesThis, false);
         }
 
         var allFormals = new List<Formal>();
@@ -9129,7 +9129,7 @@ Expression LetDesugaring(LetExpr e) {
             bool usesHeap = false, usesOldHeap = false;
             var FVsHeapAt = new HashSet<Label>();
             Type usesThis = null;
-            FreeVariablesUtil.ComputeFreeVariables(e.RHSs[0], FVs, ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis);
+            FreeVariablesUtil.ComputeFreeVariables(e.RHSs[0], FVs, ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis, false);
             var FTVs = new HashSet<TypeParameter>();
             foreach (var bv in e.BoundVars) {
               FVs.Remove(bv);
@@ -10566,7 +10566,7 @@ public static bool UsesHeap(Expression expr) {
       bool usesHeap = false, usesOldHeap = false;
       var FVsHeapAt = new HashSet<Label>();
       Type usesThis = null;
-      FreeVariablesUtil.ComputeFreeVariables(expr, new HashSet<IVariable>(), ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis);
+      FreeVariablesUtil.ComputeFreeVariables(expr, new HashSet<IVariable>(), ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis, false);
       return usesHeap || usesOldHeap || FVsHeapAt.Count != 0;
     }
 
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index 3d676f06dcc..02dabbcd57f 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -74,7 +74,6 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
                   boardSoFar <= B
                   ==>
                   (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
-  ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));
   decreases N - |boardSoFar|;
 {
   var pos := |boardSoFar|;
diff --git a/Test/allocated1/dafny0/Simple.dfy.expect b/Test/allocated1/dafny0/Simple.dfy.expect
index cc2d0771b18..a37b202e128 100644
--- a/Test/allocated1/dafny0/Simple.dfy.expect
+++ b/Test/allocated1/dafny0/Simple.dfy.expect
@@ -105,5 +105,6 @@ module B refines A {
     ...;
   }
 }
+Simple.dfy(14,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier did not attempt verification
diff --git a/Test/allocated1/dafny0/SmallTests.dfy.expect b/Test/allocated1/dafny0/SmallTests.dfy.expect
index c4572b29a50..75916a8983c 100644
--- a/Test/allocated1/dafny0/SmallTests.dfy.expect
+++ b/Test/allocated1/dafny0/SmallTests.dfy.expect
@@ -1,4 +1,5 @@
 SmallTests.dfy(548,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy(599,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 SmallTests.dfy(34,11): Error: index out of range
 SmallTests.dfy(65,35): Error: possible division by zero
 SmallTests.dfy(66,50): Error: possible division by zero
@@ -52,5 +53,6 @@ SmallTests.dfy(716,8): Error: cannot establish the existence of LHS values that
 
 Dafny program verifier finished with 51 verified, 46 errors
 SmallTests.dfy.tmp.dprint.dfy(450,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy.tmp.dprint.dfy(740,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier did not attempt verification
diff --git a/Test/allocated1/dafny0/Twostate-Verification.dfy.expect b/Test/allocated1/dafny0/Twostate-Verification.dfy.expect
index 4f8fa950122..1489e0b60cb 100644
--- a/Test/allocated1/dafny0/Twostate-Verification.dfy.expect
+++ b/Test/allocated1/dafny0/Twostate-Verification.dfy.expect
@@ -1,3 +1,4 @@
+Twostate-Verification.dfy(34,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 Twostate-Verification.dfy(39,26): Error: target object might not be allocated
 Twostate-Verification.dfy(44,34): Error: target object might not be allocated
 Twostate-Verification.dfy(60,26): Error: target object might not be allocated
diff --git a/Test/concurrency/12-MutexLifetime-long.dfy b/Test/concurrency/12-MutexLifetime-long.dfy
index 5662b23d4f4..7139e39f28c 100644
--- a/Test/concurrency/12-MutexLifetime-long.dfy
+++ b/Test/concurrency/12-MutexLifetime-long.dfy
@@ -437,7 +437,6 @@ trait OwnedObject extends Object {
 
   twostate predicate unchangedNonvolatileFields() reads this {
     && old(owner) == owner
-    && old(lifetime) == lifetime
     && unchangedNonvolatileUserFields()
   }
 
@@ -454,7 +453,6 @@ trait OwnedObject extends Object {
 
   twostate predicate localInv2() reads * {
     && (owner != null ==> localUserInv2())
-    && old(lifetime) == lifetime
   }
 
   twostate predicate sequenceInv2() reads * {
@@ -690,8 +688,7 @@ class OutlivesClaim extends OwnedObject {
   function objectUserFields(): set<Object> reads this { { source, target } }
 
   twostate predicate unchangedNonvolatileUserFields() reads this {
-    && old(target) == target
-    && old(source) == source
+    true
   }
 
   predicate localUserInv() reads * {
@@ -699,7 +696,7 @@ class OutlivesClaim extends OwnedObject {
     && universe.outlives(target, source)
   }
   predicate userInv() reads * ensures userInv() ==> localUserInv() { localUserInv() }
-  twostate predicate localUserInv2() reads * { old(target) == target && old(source) == source }
+  twostate predicate localUserInv2() reads * { true }
   twostate predicate userInv2() reads * ensures userInv2() ==> localUserInv2() { localUserInv2() }
 
   twostate lemma sequenceAdmissibility(running: set<Thread>) requires goodPreAndLegalChangesSequence(running) ensures sequenceInv2() {}
diff --git a/Test/concurrency/12-MutexLifetime-short.dfy b/Test/concurrency/12-MutexLifetime-short.dfy
index c4712c741bd..cb1b97ccbf6 100644
--- a/Test/concurrency/12-MutexLifetime-short.dfy
+++ b/Test/concurrency/12-MutexLifetime-short.dfy
@@ -436,7 +436,6 @@ trait OwnedObject extends Object {
 
   twostate predicate unchangedNonvolatileFields() reads this {
     && old(owner) == owner
-    && old(lifetime) == lifetime
     && unchangedNonvolatileUserFields()
   }
 
@@ -453,7 +452,6 @@ trait OwnedObject extends Object {
 
   twostate predicate localInv2() reads * {
     && (owner != null ==> localUserInv2())
-    && old(lifetime) == lifetime
   }
 
   twostate predicate sequenceInv2() reads * {
@@ -689,8 +687,7 @@ class OutlivesClaim extends OwnedObject {
   function objectUserFields(): set<Object> reads this { { source, target } }
 
   twostate predicate unchangedNonvolatileUserFields() reads this {
-    && old(target) == target
-    && old(source) == source
+    true
   }
 
   predicate localUserInv() reads * {
@@ -698,7 +695,7 @@ class OutlivesClaim extends OwnedObject {
     && universe.outlives(target, source)
   }
   predicate userInv() reads * ensures userInv() ==> localUserInv() { localUserInv() }
-  twostate predicate localUserInv2() reads * { old(target) == target && old(source) == source }
+  twostate predicate localUserInv2() reads * { true }
   twostate predicate userInv2() reads * ensures userInv2() ==> localUserInv2() { localUserInv2() }
 
   twostate lemma sequenceAdmissibility(running: set<Thread>) requires goodPreAndLegalChangesSequence(running) ensures sequenceInv2() {}
diff --git a/Test/concurrency/12-MutexLifetime-short.dfy.expect b/Test/concurrency/12-MutexLifetime-short.dfy.expect
index 03005235cbc..5762072e289 100644
--- a/Test/concurrency/12-MutexLifetime-short.dfy.expect
+++ b/Test/concurrency/12-MutexLifetime-short.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 204 verified, 0 errors
+Dafny program verifier finished with 202 verified, 0 errors
diff --git a/Test/dafny0/LabeledAsserts.dfy.expect b/Test/dafny0/LabeledAsserts.dfy.expect
index 62dff815b92..508bd8a60ae 100644
--- a/Test/dafny0/LabeledAsserts.dfy.expect
+++ b/Test/dafny0/LabeledAsserts.dfy.expect
@@ -1,3 +1,5 @@
+LabeledAsserts.dfy(63,9): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+LabeledAsserts.dfy(63,30): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 LabeledAsserts.dfy(25,11): Error: assertion might not hold
 LabeledAsserts.dfy(27,18): Error: assertion might not hold
 LabeledAsserts.dfy(28,18): Error: assertion might not hold
diff --git a/Test/dafny0/LabelsOldAt.dfy.expect b/Test/dafny0/LabelsOldAt.dfy.expect
index fdce8098d24..d00a750700a 100644
--- a/Test/dafny0/LabelsOldAt.dfy.expect
+++ b/Test/dafny0/LabelsOldAt.dfy.expect
@@ -1,3 +1,4 @@
+LabelsOldAt.dfy(160,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 LabelsOldAt.dfy(34,13): Error: assertion might not hold
 LabelsOldAt.dfy(56,11): Error: assertion might not hold
 LabelsOldAt.dfy(78,13): Error: assertion might not hold
diff --git a/Test/dafny0/OpaqueTypeWithMembers.dfy b/Test/dafny0/OpaqueTypeWithMembers.dfy
index aec2a4b7e96..4452fcc06c9 100644
--- a/Test/dafny0/OpaqueTypeWithMembers.dfy
+++ b/Test/dafny0/OpaqueTypeWithMembers.dfy
@@ -23,7 +23,7 @@ type Opaque {
     ensures old(a[3] + y) == y
   {
     u := old(y + a[3]);
-    var f := old(F());
+    var f := old(F()); // warning: old has no effect (since F has no reads clause)
     var u' := y + a[3];
     var f' := F();
   }
@@ -61,7 +61,7 @@ type StaticOpaque {
     ensures old(a[3] + y) == y
   {
     u := old(y + a[3]);
-    var f := old(F());
+    var f := old(F()); // warning: old has no effect (since F has no reads clause)
     var u' := y + a[3];
     var f' := F();
   }
@@ -91,7 +91,7 @@ type OpaqueErrors {
     ensures old(a[3] + y) == y
   {
     u := old(y + a[2]);  // error: index out of bounds
-    var f := old(F());
+    var f := old(F()); // warning: old has no effect (since F has no reads clause)
     var u' := y + a[2];
     var f' := F();
   }
diff --git a/Test/dafny0/OpaqueTypeWithMembers.dfy.expect b/Test/dafny0/OpaqueTypeWithMembers.dfy.expect
index 8d29e6e1bda..558bacdaaac 100644
--- a/Test/dafny0/OpaqueTypeWithMembers.dfy.expect
+++ b/Test/dafny0/OpaqueTypeWithMembers.dfy.expect
@@ -1,3 +1,6 @@
+OpaqueTypeWithMembers.dfy(26,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+OpaqueTypeWithMembers.dfy(64,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+OpaqueTypeWithMembers.dfy(94,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 OpaqueTypeWithMembers.dfy(83,36): Error: possible division by zero
 OpaqueTypeWithMembers.dfy(84,51): Error: possible division by zero
 OpaqueTypeWithMembers.dfy(87,9): Error: index out of range
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index 6fdd7bc3530..b56282d2370 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -11,7 +11,7 @@ class MyClass<T,U> {
     requires s;
     modifies this, lotsaObjects;
     ensures t == t;
-    ensures old(null) != this;
+    ensures old(null) != this; // warning: old(null) is the same as null
   {
     x := 12;
     while (x < 100)
diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect
index 54a1bc8c277..1e90daa15d3 100644
--- a/Test/dafny0/Simple.dfy.expect
+++ b/Test/dafny0/Simple.dfy.expect
@@ -105,5 +105,6 @@ greatest lemma M'(x': int)
   ensures true
 {
 }
+Simple.dfy(14,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier did not attempt verification
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 5f0e952f225..a5be04cf8c8 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -1,4 +1,5 @@
 SmallTests.dfy(548,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy(599,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 SmallTests.dfy(909,14): Error: target object might be null
 SmallTests.dfy(901,14): Error: target object might be null
 SmallTests.dfy(34,11): Error: index out of range
@@ -54,5 +55,6 @@ SmallTests.dfy(716,8): Error: cannot establish the existence of LHS values that
 
 Dafny program verifier finished with 56 verified, 48 errors
 SmallTests.dfy.tmp.dprint.dfy(450,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy.tmp.dprint.dfy(803,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier did not attempt verification
diff --git a/Test/dafny0/Twostate-Verification.dfy b/Test/dafny0/Twostate-Verification.dfy
index 357439c7adb..d20cf1dc66e 100644
--- a/Test/dafny0/Twostate-Verification.dfy
+++ b/Test/dafny0/Twostate-Verification.dfy
@@ -30,7 +30,7 @@ class A {
   }
 
   twostate lemma L2(a: A, b: A)
-    requires old(a != b)
+    requires old(a != b) // warning: old has no effect
   {}
 
   twostate lemma L3(a: A, new b: A)
@@ -653,33 +653,33 @@ module TwoStateAt {
     label Label:
 
     if * {
-      ghost var f0 := old(d0.value);
-      ghost var f1 := old(nt.value);
-      ghost var f2 := old(ot.value);
-      ghost var f3 := old(d1.value);  // error: receiver is not in old state
+      ghost var f0 := old(d0.value); // warning: old has no effect
+      ghost var f1 := old(nt.value); // warning: old has no effect
+      ghost var f2 := old(ot.value); // warning: old has no effect
+      ghost var f3 := old(d1.value);  // error: receiver is not in old state (warning: old has no effect)
     } else if * {
-      ghost var g0 := old(DT<Cell>.sc);
-      ghost var g1 := old(NT.sc);
-      ghost var g2 := old(OT<Cell>.sc);
+      ghost var g0 := old(DT<Cell>.sc); // warning: old has no effect
+      ghost var g1 := old(NT.sc); // warning: old has no effect
+      ghost var g2 := old(OT<Cell>.sc); // warning: old has no effect
     } else if * {
-      ghost var h0 := old(d0.sc);
-      ghost var h1 := old(nt.sc);
-      ghost var h2 := old(ot.sc);
-      ghost var h3 := old(d1.sc);  // this is also fine
+      ghost var h0 := old(d0.sc); // warning: old has no effect
+      ghost var h1 := old(nt.sc); // warning: old has no effect
+      ghost var h2 := old(ot.sc); // warning: old has no effect
+      ghost var h3 := old(d1.sc);  // this is also fine (warning: old has no effect)
     } else if * {
-      ghost var f0 := old@Label(d0.value);
-      ghost var f1 := old@Label(nt.value);
-      ghost var f2 := old@Label(ot.value);
-      ghost var f3 := old@Label(d1.value);  // fine
+      ghost var f0 := old@Label(d0.value); // warning: old has no effect
+      ghost var f1 := old@Label(nt.value); // warning: old has no effect
+      ghost var f2 := old@Label(ot.value); // warning: old has no effect
+      ghost var f3 := old@Label(d1.value);  // fine (warning: old has no effect)
     } else if * {
-      ghost var g0 := old@Label(DT<Cell>.sc);
-      ghost var g1 := old@Label(NT.sc);
-      ghost var g2 := old@Label(OT<Cell>.sc);
+      ghost var g0 := old@Label(DT<Cell>.sc); // warning: old has no effect
+      ghost var g1 := old@Label(NT.sc); // warning: old has no effect
+      ghost var g2 := old@Label(OT<Cell>.sc); // warning: old has no effect
     } else if * {
-      ghost var h0 := old@Label(d0.sc);
-      ghost var h1 := old@Label(nt.sc);
-      ghost var h2 := old@Label(ot.sc);
-      ghost var h3 := old@Label(d1.sc);
+      ghost var h0 := old@Label(d0.sc); // warning: old has no effect
+      ghost var h1 := old@Label(nt.sc); // warning: old has no effect
+      ghost var h2 := old@Label(ot.sc); // warning: old has no effect
+      ghost var h3 := old@Label(d1.sc); // warning: old has no effect
     }
   }
 }
diff --git a/Test/dafny0/Twostate-Verification.dfy.expect b/Test/dafny0/Twostate-Verification.dfy.expect
index d627df2ecb2..8815ae6a4e1 100644
--- a/Test/dafny0/Twostate-Verification.dfy.expect
+++ b/Test/dafny0/Twostate-Verification.dfy.expect
@@ -1,3 +1,26 @@
+Twostate-Verification.dfy(656,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(657,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(658,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(659,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(661,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(662,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(663,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(665,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(666,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(667,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(668,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(670,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(671,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(672,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(673,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(675,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(676,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(677,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(679,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(680,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(681,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(682,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Twostate-Verification.dfy(33,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 Twostate-Verification.dfy(271,13): Error: A postcondition might not hold on this return path.
 Twostate-Verification.dfy(263,24): Related location: This is the postcondition that might not hold.
 Twostate-Verification.dfy(277,4): Error: A postcondition might not hold on this return path.
diff --git a/Test/dafny0/TypeMembers.dfy b/Test/dafny0/TypeMembers.dfy
index f10f5a9ce47..0249e7edfb2 100644
--- a/Test/dafny0/TypeMembers.dfy
+++ b/Test/dafny0/TypeMembers.dfy
@@ -112,7 +112,7 @@ datatype Dt<A> = Blue | Bucket(diameter: real) | Business(trendy: bool, a: A)
   static method P(x: int) returns (y: int) {
     y := x + g;
   }
-  twostate predicate Toop() { old(this) == this }
+  twostate predicate Toop() { old(this) == this } // warning: old has no effect
   twostate lemma Tool() { }
   least predicate IndP() { true }
   greatest predicate CoP() { true }
diff --git a/Test/dafny0/TypeMembers.dfy.expect b/Test/dafny0/TypeMembers.dfy.expect
index 6967cc6d1f6..4ae15093915 100644
--- a/Test/dafny0/TypeMembers.dfy.expect
+++ b/Test/dafny0/TypeMembers.dfy.expect
@@ -1,3 +1,4 @@
+TypeMembers.dfy(115,30): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier finished with 29 verified, 0 errors
 DaTy.Yes 10 26
diff --git a/Test/git-issues/git-issue-1163.dfy b/Test/git-issues/git-issue-1163.dfy
index 9bb2dd9cdfa..b747ae32c58 100644
--- a/Test/git-issues/git-issue-1163.dfy
+++ b/Test/git-issues/git-issue-1163.dfy
@@ -4,7 +4,7 @@
 function F(i: int): int
 
 method M() {
-  ghost var f := old(i => F(i));  // the translation of this once had crashed the verifier
+  ghost var f := old(i => F(i));  // the translation of this once had crashed the verifier (warning: old has no effect)
 }
 
 class MyClass {
diff --git a/Test/git-issues/git-issue-1163.dfy.expect b/Test/git-issues/git-issue-1163.dfy.expect
index 081e4dbdad7..3f619a04c07 100644
--- a/Test/git-issues/git-issue-1163.dfy.expect
+++ b/Test/git-issues/git-issue-1163.dfy.expect
@@ -1,3 +1,4 @@
+git-issue-1163.dfy(7,17): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 git-issue-1163.dfy(21,42): Error: receiver argument might not be allocated in the state in which the function is invoked
 git-issue-1163.dfy(23,44): Error: argument might not be allocated in the state in which the function is invoked
 git-issue-1163.dfy(27,40): Error: receiver argument might not be allocated in the state in which the function is invoked
diff --git a/Test/git-issues/git-issue-1989.dfy b/Test/git-issues/git-issue-1989.dfy
new file mode 100644
index 00000000000..aa1e1b3f318
--- /dev/null
+++ b/Test/git-issues/git-issue-1989.dfy
@@ -0,0 +1,238 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// ---------------------------------------
+
+module Test {
+  class C {
+  }
+
+  function arrSet(a: array<C>): set<object>
+    reads a
+  {
+    set i : int | 0 <= i < a.Length :: a[i]
+  }
+
+  method test(a: array<C>, i: int, x: C)
+    modifies a
+    requires 0 <= i < a.Length
+    requires x !in arrSet(a)
+  {
+    a[i] := x;
+    assert arrSet(a) == arrSet(old(a)); // warning: old has no effect
+  }
+}
+
+// ---------------------------------------
+
+predicate P(s: seq<int>)
+predicate Q(a: array<int>)
+  reads a
+
+class C {
+  var x: int
+
+  predicate PInClass(s: seq<int>)
+  static predicate StaticPInClass(s: seq<int>)
+
+  predicate QInClass(a: array<int>)
+    reads a
+  static predicate StaticQInClass(a: array<int>)
+    reads a
+
+  predicate R(y: int := x)
+    reads this
+}
+
+method TestsNoReads(c: C, s: seq<int>, a: array<int>) {
+  ghost var b;
+  b := old(P(s)); // warning: old has no effect
+  b := old(c.PInClass(s)); // warning: old has no effect
+  b := old(C.StaticPInClass(s)); // warning: old has no effect
+  b := old(c.StaticPInClass(s)); // warning: old has no effect
+
+  b := old(Q(a));
+  b := old(c.QInClass(a));
+  b := old(C.StaticQInClass(a));
+  b := old(c.StaticQInClass(a));
+
+  b := old(c.R(3));
+  b := old(c.R());
+}
+
+method Trigger()
+  // The following should generate a warning, but preferably not two.
+  // That is, if the old expression is copied into the trigger, it
+  // is preferable that there's not a second warning for the 'old' there.
+  ensures forall s :: P(s) == old(P(s)) // warning: old has no effect
+
+  // A manually supplied trigger should have its own warning, though:
+  ensures forall s {:trigger old(P(s))} :: P(s) == old(P(s)) // warning (x2): old has no effect
+{
+}
+
+// An iterator has several auto-generated old expressions.
+// These should not generate any warnings.
+iterator Iter()
+{
+}
+
+// ---------------------------------------
+
+class D {
+  var data: int
+  const N: int
+  var arr: array<real>
+
+  method TestFields()
+    ensures data == old(data)
+    ensures N == old(N) // warning: old has no effect, since N is const
+  {
+  }
+
+  method TestArrayElements(j: nat, a: array<real>)
+    requires j < a.Length
+    ensures a.Length == old(a.Length) // warning: old has no effect
+    ensures a[j] == old(a[j])
+    ensures a[j] == old(a)[j] // warning: old has no effect
+    ensures a[j] == a[old(j)] // warning: old has no effect
+  {
+  }
+
+  method MoreArrays(b: array<real>)
+    requires 0 <= data && data + 1 < arr.Length == b.Length
+    requires 1.0 <= arr[data] < arr[data + 1] < 2.0
+    requires 4.0 <= b[data] < b[data + 1] < 5.0
+    modifies this, arr
+    ensures arr == b && data == old(data) + 1
+    ensures arr[data] != old(arr[data])
+    ensures arr[data] != old(arr)[data]
+    ensures arr[data] != arr[old(data)]
+    ensures var a, j := arr, data; old(arr[data]) != old(a[j])
+  {
+    forall i | 0 <= i < arr.Length {
+      arr[i] := 2.0 * arr[i];
+    }
+    arr := b;
+    data := data + 1;
+  }
+
+  method TestMatrixElements(i: nat, j: nat, m: array2<real>)
+    requires i < m.Length0 && j < m.Length1
+    ensures m.Length0 == old(m.Length1) // warning: old has no effect
+    ensures m[i, j] == old(m[i, j])
+    ensures m[i, j] == old(m)[i, j] // warning: old has no effect
+    ensures m[i, j] == m[i, old(j)] // warning: old has no effect
+  {
+  }
+
+  lemma Lemma(y: int)
+    requires data == y
+  {
+  }
+}
+
+
+lemma StaticLemmaWithoutPrecondition(y: int)
+{
+}
+
+// ---------------------------------------
+
+method StmtExpr(d: D)
+  requires d.data == 3
+  modifies d
+{
+  ghost var a;
+  d.data := 100;
+  if {
+  case true =>
+    a := assert d.data < 5; 10; // error: assertion failure
+  case true =>
+    a := old(20 + assert d.data < 5; 10);
+  case true =>
+    a := old(d.Lemma(3); 10);
+  case true =>
+    a := old(d.Lemma(100); 10); // error: precondition violation
+  case true =>
+    a := (d.Lemma(old(100)); 10); // warning: old has no effect
+  }
+  a := assert d.data < old(105); 0; // warning: old has no effect
+}
+
+method CalcStmtExpr(d: D)
+  requires d.data == 3
+  modifies d
+{
+  ghost var a;
+  d.data := 100;
+  if {
+  case true =>
+    a := old(calc { } 10); // warning: old has no effect
+  case true =>
+    a := old(calc {
+      2;
+    ==  { assert d.data == 3; }
+      2;
+    } 10);
+  case true =>
+    a := old(calc {
+      2;
+    ==  { assert d.data == 100; } // error: assertion violation
+      2;
+    } 10);
+  case true =>
+    a := old(calc {
+      2;
+    ==  { d.Lemma(3); }
+      2;
+    } 10);
+  case true =>
+    a := old(calc {
+      2;
+    ==  { StaticLemmaWithoutPrecondition(3); }
+      2;
+    } 10);
+  case true =>
+    a := old(calc {
+      2;
+    ==  { d.Lemma(100); } // error: precondition violation
+      2;
+    } 10);
+  }
+}
+
+twostate function CalcStmtExprFunction(d: D, selector: int): int
+  requires old(d.data) == 3 && d.data == 100
+  reads d
+{
+  match selector
+  case 0 =>
+    old(calc { } 10) // warning: old has no effect
+  case 1 =>
+    old(calc {
+      2;
+    ==  { assert d.data == 3; }
+      2;
+    } 10)
+  case 2 =>
+    old(calc {
+      2;
+    ==  { assert d.data == 100; } // error: assertion violation
+      2;
+    } 10)
+  case 3 =>
+    old(calc {
+      2;
+    ==  { d.Lemma(3); }
+      2;
+    } 10)
+  case 4 =>
+    old(calc {
+      2;
+    ==  { d.Lemma(100); } // error: precondition violation
+      2;
+    } 10)
+  case _ =>
+    10
+}
diff --git a/Test/git-issues/git-issue-1989.dfy.expect b/Test/git-issues/git-issue-1989.dfy.expect
new file mode 100644
index 00000000000..d29adadafef
--- /dev/null
+++ b/Test/git-issues/git-issue-1989.dfy.expect
@@ -0,0 +1,31 @@
+git-issue-1989.dfy(22,31): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(89,17): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(97,20): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(98,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(124,23): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(125,28): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(49,7): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(50,7): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(51,7): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(52,7): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(67,30): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(70,29): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(70,29): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(70,51): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(158,18): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(160,23): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(171,9): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(211,4): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+git-issue-1989.dfy(126,2): Error: A postcondition might not hold on this return path.
+git-issue-1989.dfy(122,22): Related location: This is the postcondition that might not hold.
+git-issue-1989.dfy(150,23): Error: assertion might not hold
+git-issue-1989.dfy(156,20): Error: A precondition for this call might not hold.
+git-issue-1989.dfy(130,18): Related location: This is the precondition that might not hold.
+git-issue-1989.dfy(181,24): Error: assertion might not hold
+git-issue-1989.dfy(199,17): Error: A precondition for this call might not hold.
+git-issue-1989.dfy(130,18): Related location: This is the precondition that might not hold.
+git-issue-1989.dfy(221,24): Error: assertion might not hold
+git-issue-1989.dfy(233,17): Error: A precondition for this call might not hold.
+git-issue-1989.dfy(130,18): Related location: This is the precondition that might not hold.
+
+Dafny program verifier finished with 17 verified, 7 errors
diff --git a/Test/refman/Example-Old.dfy.expect b/Test/refman/Example-Old.dfy.expect
index 823a60a105c..a4fdc907b7e 100644
--- a/Test/refman/Example-Old.dfy.expect
+++ b/Test/refman/Example-Old.dfy.expect
@@ -1,2 +1,5 @@
+Example-Old.dfy(16,11): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Example-Old.dfy(17,11): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+Example-Old.dfy(18,11): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Test/refman/Example-Old3.dfy.expect b/Test/refman/Example-Old3.dfy.expect
index ebe2328e072..c6d44b46b7b 100644
--- a/Test/refman/Example-Old3.dfy.expect
+++ b/Test/refman/Example-Old3.dfy.expect
@@ -1,2 +1,3 @@
+Example-Old3.dfy(18,11): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/traits/TraitOverride2.dfy b/Test/traits/TraitOverride2.dfy
index 1cb04f46272..41ca3e82bc4 100644
--- a/Test/traits/TraitOverride2.dfy
+++ b/Test/traits/TraitOverride2.dfy
@@ -16,7 +16,6 @@ trait Spec<U> {
     requires Valid()
     modifies Repr
     ensures Valid()
-    ensures Repr == old(Repr)
     decreases Repr
 }
 
@@ -46,7 +45,6 @@ class Impl<T> extends Spec<T> {
     requires Valid()
     modifies Repr
     ensures Valid()
-    ensures Repr == old(Repr)
     decreases Repr
   {
     if done || hasFailed {
@@ -82,7 +80,6 @@ class AnotherImpl<T> extends Spec<seq<T>> {
     requires Valid()
     modifies Repr
     ensures Valid()
-    ensures Repr == old(Repr)
     decreases Repr
   { }
 }
@@ -106,6 +103,5 @@ class FixedImpl extends Spec<int> {
     requires Valid()
     modifies Repr
     ensures Valid()
-    ensures Repr == old(Repr)
     decreases Repr
 }
diff --git a/Test/traits/TraitOverride2.dfy.expect b/Test/traits/TraitOverride2.dfy.expect
index 842d05da0e6..4bb1c2c7251 100644
--- a/Test/traits/TraitOverride2.dfy.expect
+++ b/Test/traits/TraitOverride2.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 20 verified, 0 errors
+Dafny program verifier finished with 18 verified, 0 errors
diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
index 161e9c4940a..a21cfa29a4b 100644
--- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
@@ -12,7 +12,7 @@
 // experiences could cause a change of mind.
 
 class C { }
-function f(c: C): C
+function f(c: C): C reads c
 function g(c: C): C
 function h(c: C, i: int): C
 
diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy b/Test/triggers/old-is-a-special-case-for-triggers.dfy
index fd537f4d82e..98cafb29c19 100644
--- a/Test/triggers/old-is-a-special-case-for-triggers.dfy
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy
@@ -12,21 +12,40 @@ function h(c: C, i: int): C
 
 method M(sc: set<C>)
   // Ensure that old(c) does not get picked as a trigger
-  ensures forall c | c in sc :: true || c == old(f(c))
+  ensures forall c | c in sc :: true || c == old(f(c)) // warning: old has no effect
 
   // This checks whether loop detection handles `old` expressions properly.
   // In the first one f(c)/old(f(f(c))) is not reported as a loop. See
   // looping-is-hard-to-decide-modulo-equalities.dfy for an explanation.
-  ensures forall c | c in sc :: true || f(c) == old(f(f(c)))
-  ensures forall c | c in sc :: true || old(f(f(c))) == old(g(f(c))) || old(f(g(c))) == g(f(c)) || f(g(c)) == g(f(c))
+  ensures forall c | c in sc :: true || f(c) == old(f(f(c))) // warning: old has no effect
+  ensures forall c | c in sc :: true || old(f(f(c))) == old(g(f(c))) || old(f(g(c))) == g(f(c)) || f(g(c)) == g(f(c)) // warning (x3): old has no effect
 
   // These check that the final trigger filtering step doesn't get confused
   // between old expressions and regular expressions.
-  ensures forall c | c in sc :: true || f(c) == old(g(f(c)))
-  ensures forall c | c in sc :: true || f(c) == old(f(c)) || old(g(f(c))) == g(f(c))
+  ensures forall c | c in sc :: true || f(c) == old(g(f(c))) // warning: old has no effect
+  ensures forall c | c in sc :: true || f(c) == old(f(c)) || old(g(f(c))) == g(f(c)) // warning (x2): old has no effect
 
   // WISH: A Dafny rewriter could cleanup expressions so that adding the
   //       expression forall c :: c == old(c) in a quantifier would cause a warning,
   //       instead of a trigger generation error as it does now.
 {
 }
+
+function ff(c: C): C reads c
+
+method MM(sc: set<C>)
+  // Ensure that old(c) does not get picked as a trigger
+  ensures forall c | c in sc :: true || c == old(ff(c))
+
+  // This checks whether loop detection handles `old` expressions properly.
+  // In the first one ff(c)/old(ff(ff(c))) is not reported as a loop. See
+  // looping-is-hard-to-decide-modulo-equalities.dfy for an explanation.
+  ensures forall c | c in sc :: true || ff(c) == old(ff(ff(c)))
+  ensures forall c | c in sc :: true || old(ff(ff(c))) == old(g(ff(c))) || old(ff(g(c))) == g(ff(c)) || ff(g(c)) == g(ff(c))
+
+  // These check that the final trigger filtering step doesn't get confused
+  // between old expressions and regular expressions.
+  ensures forall c | c in sc :: true || ff(c) == old(g(ff(c)))
+  ensures forall c | c in sc :: true || ff(c) == old(ff(c)) || old(g(ff(c))) == g(ff(c))
+{
+}
diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
index 8399e6be6ce..f86863bf654 100644
--- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
@@ -18,5 +18,33 @@ old-is-a-special-case-for-triggers.dfy(26,10): Info: Selected triggers:
  Rejected triggers:
    {g(f(c))} (more specific than {f(c)})
    {old(g(f(c)))} (more specific than {old(f(c))})
+old-is-a-special-case-for-triggers.dfy(38,10): Info: Selected triggers:
+   {old(ff(c))}, {c in sc}
+old-is-a-special-case-for-triggers.dfy(43,10): Info: Selected triggers:
+   {old(ff(ff(c)))}, {ff(c)}, {c in sc}
+ Rejected triggers: {old(ff(c))} (may loop with "old(ff(ff(c)))")
+old-is-a-special-case-for-triggers.dfy(44,10): Info: Selected triggers:
+   {ff(g(c))}, {g(ff(c))}, {old(ff(g(c)))}, {old(g(ff(c)))}, {old(ff(ff(c)))}, {c in sc}
+ Rejected triggers:
+   {g(c)} (may loop with "g(ff(c))")
+   {ff(c)} (may loop with "ff(g(c))")
+   {old(g(c))} (may loop with "old(g(ff(c)))")
+   {old(ff(c))} (may loop with "old(ff(ff(c)))", "old(ff(g(c)))")
+old-is-a-special-case-for-triggers.dfy(48,10): Info: Selected triggers:
+   {old(ff(c))}, {ff(c)}, {c in sc}
+ Rejected triggers: {old(g(ff(c)))} (more specific than {old(ff(c))})
+old-is-a-special-case-for-triggers.dfy(49,10): Info: Selected triggers:
+   {old(ff(c))}, {ff(c)}, {c in sc}
+ Rejected triggers:
+   {g(ff(c))} (more specific than {ff(c)})
+   {old(g(ff(c)))} (more specific than {old(ff(c))})
+old-is-a-special-case-for-triggers.dfy(15,45): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(20,48): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(21,40): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(21,56): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(21,72): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(25,48): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(26,48): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+old-is-a-special-case-for-triggers.dfy(26,61): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 4 verified, 0 errors