Make `old` a special case for trigger generation.

Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and
old(f(x)). This has a number of implications; see the new tests files for more
information.

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 230d9349..557eee93 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -47,10 +47,10 @@ namespace Microsoft.Dafny
       var finder = new Triggers.QuantifierCollector(reporter);

         

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

-        finder.Visit(decl, null);

+        finder.Visit(decl, false);

       }

       

-      var triggersCollector = new Triggers.TriggersCollector();

+      var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext);

       foreach (var quantifierCollection in finder.quantifierCollections) {

         quantifierCollection.ComputeTriggers(triggersCollector);

         quantifierCollection.CommitTriggers();