diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:39:02 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:39:02 -0700 |
| commit | 2db858bf6e72e521b49aa0ae3a993dc943b8c875 (patch) | |
| tree | 692ebe07028e35e431e8b93ee35266461126d5cd /Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect | |
| parent | 3b1c3923a403efbd28b8f5ae6fc4429ccee8c2e8 (diff) | |
Implement {:nowarn}, clarify some messages, and add a few tests
Diffstat (limited to 'Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect')
| -rw-r--r-- | Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect index 6b152262..6c3e4853 100644 --- a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect @@ -1,16 +1,16 @@ -wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {0 <= f(n)}:
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "0 <= f(n)":
Selected triggers: {f(n)}
Rejected triggers: {P(f(n))} (more specific than {f(n)})
-wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {P(f(n))}:
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "P(f(n))":
Selected triggers: {f(n)}
Rejected triggers: {P(f(n))} (more specific than {f(n)})
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c != null}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c != null":
Selected triggers:
{c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c' != null}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c' != null":
Selected triggers:
{c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c.x == c'.x}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c.x == c'.x":
Selected triggers:
{c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
|