From 1a78514315cd88463845d32a7bf237cb7a3eb063 Mon Sep 17 00:00:00 2001
From: Tony Knapp <5892063+texastony@users.noreply.github.com>
Date: Wed, 27 Jul 2022 16:39:03 -0500
Subject: [PATCH] chore: address dafny-lang/dafny#2500  (#599)

---
 .github/PULL_REQUEST_TEMPLATE.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index c23fc89fd..8427e3636 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -6,3 +6,20 @@
 
 
 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
+
+# Due to [dafny-lang/dafny#2500](https://github.com/dafny-lang/dafny/issues/2500), Traits are dangerous:
+1. [ ] Does this PR add any traits or classes that extend a trait?
+2. [ ] Are these traits annotated with `{:termination false}`?
+
+The override checks on 
+the specifications on
+a class' functions/methods/etc. validating
+that specifications are 
+at least as strong as those on
+the traits it implements
+are not working correctly when 
+that trait is defined in a different module 
+(and hence must have `{:termination false}` on it).
+
+As such, if either (1.) or (2.) is true:
+- [ ] manually verified all the trait specifications are copied onto classes that extend them?