When an Expr immutable, never change Type reference if it has been set,

even if the types are equivalent.

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;

         }

       }

     }