diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-26 18:36:34 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-26 18:36:34 -0700 |
commit | c55cb226f4de90b080aa809d883d52c3386db063 (patch) | |
tree | 47c5d8dd0c9e62983ad752adda07cf532b3a1a4f /Test/triggers/redundancy-detection-is-bidirectional.dfy.expect | |
parent | aa13b513cd70fd39ae9eb9ddc2621fb8747f89ff (diff) |
Improve the redundancy detection algorithm used while constructing sets of terms
Based on an issue noted by Chris with redundancy removal resuls being dependent
on the order of the terms. Interestingly, one of our tests already had an
instance of that problem.
Also fix the issue with nested quantifiers getting redundant triggers.
Diffstat (limited to 'Test/triggers/redundancy-detection-is-bidirectional.dfy.expect')
-rw-r--r-- | Test/triggers/redundancy-detection-is-bidirectional.dfy.expect | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect new file mode 100644 index 00000000..78c9e7ca --- /dev/null +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect @@ -0,0 +1,12 @@ +redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:
+ {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:
+ {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:
+ {P(x, y)}, {R(x), Q(y)}
+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+
+Dafny program verifier finished with 11 verified, 0 errors
|