summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-12 11:04:51 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-12 11:04:51 +0000
commitd2f542ffeecddf36004f94729745e4ba9d7d300a (patch)
tree5b9b9d7a43bdda0e8781118ab6df287ca77d8b5e /Source
parent1f8368fd50c720fe8080d6724e8bbfaecb6f486d (diff)
When an Expr immutable, never change Type reference if it has been set,
even if the types are equivalent.
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/AbsyExpr.cs5
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 3938e396..7557a796 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -104,7 +104,10 @@ namespace Microsoft.Boogie {
if (Immutable && !_Type.Equals(value))
throw new InvalidOperationException("Cannot change the Type of an Immutable Expr");
- _Type = value;
+ // Once the Type has been set (i.e. no longer null) we never change the reference
+ // if this Expr is immutable, even if the Type is equivalent (i.e. _Type.Equals(newType))
+ if (!Immutable)
+ _Type = value;
}
}
}