summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasure.cs
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-08-18 00:13:29 +0000
committerGravatar MichalMoskal <unknown>2010-08-18 00:13:29 +0000
commita54af4e97ccf24b7bd8802d7411b67bc2b4c5e55 (patch)
treed45fdf422341f6b8df670c0bd8b3e7c5fff9b782 /Source/VCExpr/TypeErasure.cs
parent94b94b49c7efdf737c6b54fb6d7ae9dd2ab189e4 (diff)
Make /typeEncoding:m work with arrays
Diffstat (limited to 'Source/VCExpr/TypeErasure.cs')
-rw-r--r--Source/VCExpr/TypeErasure.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index c4deb76c..5029ba53 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -727,7 +727,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
[Pure]
public override bool UnchangedType(Type type) {
Contract.Requires(type != null);
- return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.UseArrayTheory);
+ return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
}
public VCExpr Cast(VCExpr expr, Type toType) {