Include an explicit trigger to make NumberRepresentations.dfy behave more consistently. (There is a future opportunity to heuristically figure out such triggers.)

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index 5b7f3a0f..440a4de9 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -163,7 +163,7 @@ lemma TrimProperty(a: seq<int>)
   requires a == trim(a);

   ensures a == [] || a[1..] == trim(a[1..]);

 {

-  assert forall b :: |trim(b)| <= |b|;

+  assert forall b {:trigger trim(b)} :: |trim(b)| <= |b|;

 }

 

 lemma TrimPreservesValue(digits: seq<int>, base: nat)