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/Array.dfy           | 4 +++-
 Test/dafny0/ComputationsNeg.dfy | 2 +-
 Test/dafny0/MultiSets.dfy       | 5 ++++-
 3 files changed, 8 insertions(+), 3 deletions(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 391ca5f7..309e9248 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class A {
@@ -327,3 +327,5 @@ module DtypeRegression {
     }
   }
 }
+
+// WISH: autoTriggers disabled because of induction
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);
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index 3535f857..ba075fc3 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method test1()
@@ -295,3 +295,6 @@ lemma Set_and_Multiset_Cardinalities(x: int, y: int)
     assert |multiset{x,y}| == 2;
   }
 }
+
+// AutoTriggers explicitly removed, as simplifications of set expressions such
+// as x in {1,2} cause invalid terms to appear in the triggers
-- 
cgit v1.2.3