From c28ad1d1565e60dfd14164366552efb18876872f Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 12 Aug 2014 15:31:45 -0700
Subject: Rewrote two tests to make triggering better (while waiting for better
 automatic triggering support in either Dafny or Boogie)

---
 Test/dafny3/SimpleCoinduction.dfy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index 5be5c569..00e598c3 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -35,13 +35,13 @@ colemma {:induction false} CoUpLemma(n: int)
   CoUpLemma(n+1);
 }
 
-lemma UpLemma_Auto(k: nat, n: int)
-  ensures Inc(Up(n)) ==#[k] Up(n+1);
+lemma UpLemma_Auto(k: nat, n: int, nn: int)
+  ensures nn == n+1 ==> Inc(Up(n)) ==#[k] Up(nn);  // note: it would be nice to do an automatic rewrite (from "ensures Inc(Up(n)) ==#[k] Up(n+1)") to obtain the good trigger here
 {
 }
 
-colemma CoUpLemma_Auto(n: int)
-  ensures Inc(Up(n)) == Up(n+1);
+colemma CoUpLemma_Auto(n: int, nn: int)
+  ensures nn == n+1 ==> Inc(Up(n)) == Up(nn);  // see comment above
 {
 }
 
-- 
cgit v1.2.3