summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 15:58:36 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 15:58:36 -0700
commitc311617de4641a4eef54a0ce1bc51574effa2756 (patch)
treed48910c77b9910929a94434eeb7f7b449d950595 /Source/Dafny/Triggers
parent165aa64949e964a24ac07b32fbe114e96975c5f6 (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.cs2
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;
}