summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 10:51:44 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 10:51:44 -0700
commit674e30357980e1192ac532f4bd16c529cedc7fdc (patch)
tree583d3eca7e0d40bb4753f25d4dbb3069e3dea9b5 /Test/dafny0
parent8a0df70ffb8d57d1bd210ce2e1c9522ba0967365 (diff)
Draft out a more advanced version of trigger generation
This new version will include a cleaner pipeline, and trigger splitting.
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/SeqFromArray.dfy.expect3
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect
index af845d3e..5395e298 100644
--- a/Test/dafny0/SeqFromArray.dfy.expect
+++ b/Test/dafny0/SeqFromArray.dfy.expect
@@ -1,3 +1,6 @@
+SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.
+SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.
+SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.
Dafny program verifier finished with 10 verified, 0 errors
Program compiled successfully