1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 850fa4c1..d1b04b1d 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -219,6 +219,19 @@ module InductivePredicateResolutionErrors {
       h < 0 && CoLetSuchThat(s.tail)  // error: recursive call to copredicate in body of let-such-that
   }
 
+  inductive predicate NegatedLetSuchThat(s: List<int>)
+  {
+    if s != Nil then true else
+      !var h :| h == s.head;
+      h < 0 && !NegatedLetSuchThat(s.tail)  // error: recursive call to inductive predicate in body of let-such-that
+  }
+  copredicate NegatedCoLetSuchThat(s: IList<int>)
+  {
+    if s != INil then true else
+      !var h :| h == s.head;
+      h < 0 && !NegatedCoLetSuchThat(s.tail)  // this is fine for a coinductive predicate
+  }
+
   inductive predicate CP(i: int)
   {
     CP(i) &&