Dafny: for refinements, don't consider a newly provided predicate body to be an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c558dd14..a4d0eba1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -660,7 +660,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   ]

   (. if (isPredicate) {

         f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

-                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

+                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);

      } else if (isCoPredicate) {

         f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

                           reqs, reads, ens, body, attrs, signatureOmitted);