diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-31 10:38:55 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-31 10:38:55 +0000 |
| commit | 964ee79dcfd492afd6c4a7c21b67089b76cd78e0 (patch) | |
| tree | c0c1c4d0544369c81ad16fe7e697087c63bade53 /Source/Core/AbsyExpr.cs | |
| parent | d3e7cf42294a44b53bb7dc29ea24eff85b836bf0 (diff) | |
Fix typechecking immutable Expr when we have
<bool> == <bool>
or
<bool> != <bool>
The type checker tries rewrite the Expr when it gets type checked
which breaks immutability so disable doing this if the Expr is
immutable.
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 1b5cc3d4..3c3c8e42 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1756,7 +1756,8 @@ namespace Microsoft.Boogie { public void ResolveOverloading(NAryExpr expr) {
//Contract.Requires(expr != null);
- if (DoNotResolveOverloading)
+ // immutable Expr must not be modified
+ if (DoNotResolveOverloading || expr.Immutable)
{
return;
}
|