3 files changed, 8 insertions, 3 deletions
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