diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:14:56 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:14:56 -0700 |
| commit | dd4f127f36ec24fbcedaaae0e61e0894b2bf5e83 (patch) | |
| tree | 6e4bedc31835e51844ef2dc910372c9330016e58 /Source/Dafny/Triggers/QuantifiersCollection.cs | |
| parent | 79679075d54060ec78a369879f7ec460d30f92f4 (diff) | |
Print matches for triggers as they appear in the buffer
Triggers themselves, however, are printed exactly as used. For example, a term
(x !in s) yields a trigger (x in s).
Diffstat (limited to 'Source/Dafny/Triggers/QuantifiersCollection.cs')
| -rw-r--r-- | Source/Dafny/Triggers/QuantifiersCollection.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index a6340f10..49cd84df 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -118,7 +118,7 @@ namespace Microsoft.Dafny.Triggers { c => !loopingSubterms[c].Any(),
c => {
looping.Add(c);
- c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", ");
+ c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
}).ToList();
q.CouldSuppressLoops = safe.Count > 0;
|