diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 15:58:36 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 15:58:36 -0700 |
| commit | c311617de4641a4eef54a0ce1bc51574effa2756 (patch) | |
| tree | d48910c77b9910929a94434eeb7f7b449d950595 /Source/Dafny/Triggers | |
| parent | 165aa64949e964a24ac07b32fbe114e96975c5f6 (diff) | |
Fix the equality test for literal expressions
(compare by value, not by reference to boxed value)
Diffstat (limited to 'Source/Dafny/Triggers')
| -rw-r--r-- | Source/Dafny/Triggers/TriggerExtensions.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 0a0ad547..a49ed13a 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -477,7 +477,7 @@ namespace Microsoft.Dafny.Triggers { }
private static bool ShallowEq(LiteralExpr expr1, LiteralExpr expr2) {
- if (expr1.Value != expr2.Value) {
+ if (!TriggerUtils.SameNullity(expr1.Value, expr2.Value) || (expr1.Value != null && !expr1.Value.Equals(expr2.Value))) {
return false;
}
|