1 files changed, 5 insertions, 4 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3688ed3f..b9ad41a3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7956,9 +7956,6 @@ namespace Microsoft.Dafny {
         string msg;
         if (s.InferredDecreases) {
           msg = "cannot prove termination; try supplying a decreases clause for the loop";
-          if (s is RefinedWhileStmt) {
-            msg += " (note that a refined loop does not inherit 'decreases *' from the refined loop)";
-          }
         } else {
           msg = "decreases expression might not decrease";
         }
@@ -8356,6 +8353,10 @@ namespace Microsoft.Dafny {
       var types1 = new List<Type>();
       var callee = new List<Expr>();
       var caller = new List<Expr>();
+      if (RefinementToken.IsInherited(tok, currentModule) && contextDecreases.All(e => !RefinementToken.IsInherited(e.tok, currentModule))) {
+        // the call site is inherited but all the context decreases expressions are new
+        tok = new ForceCheckToken(tok);
+      }
       for (int i = 0; i < N; i++) {
         Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);
         Expression e1 = contextDecreases[i];
@@ -8363,7 +8364,7 @@ namespace Microsoft.Dafny {
           N = i;
           break;
         }
-        toks.Add(tok);
+        toks.Add(new NestedToken(tok, e1.tok));
         types0.Add(e0.Type.NormalizeExpand());
         types1.Add(e1.Type.NormalizeExpand());
         callee.Add(etranCurrent.TrExpr(e0));