From f3cfd7a9994af3518655bc4d1d77eeb3619b0999 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 28 Aug 2015 21:05:19 -0700
Subject: Implement workarounds for some tests that fail with /autoTriggers.

The issues here are mostly with induction (wrt. to trigger selection and
quantifier splitting) and with expressions like P(i, j-1) where no good choices
are available.
---
 Test/dafny0/ComputationsNeg.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/dafny0/ComputationsNeg.dfy')

diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
index 0c539117..b9425d64 100644
--- a/Test/dafny0/ComputationsNeg.dfy
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -16,7 +16,7 @@ predicate ThProperty(step: nat, t: Nat, r: nat)
 {
   match t
   case Zero => true
-  case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+  case Succ(o) => step>0 && exists ro:nat, ss :: ss == step-1 ==> ThProperty(ss, o, ro) // WISH: auto-generate ss
 }
 ghost method test_ThProperty()
   ensures ThProperty(10, Succ(Zero), 0);
-- 
cgit v1.2.3