summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasurePremisses.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/TypeErasurePremisses.cs
parent94b94b49c7efdf737c6b54fb6d7ae9dd2ab189e4 (diff)
Make /typeEncoding:m work with arrays
Diffstat (limited to 'Source/VCExpr/TypeErasurePremisses.cs')
-rw-r--r--Source/VCExpr/TypeErasurePremisses.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 9d5eef26..cf0bcaa4 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -634,7 +634,7 @@ Contract.Requires(var != null);
mapTypeParams.Add(var);
}
- if (CommandLineOptions.Clo.UseArrayTheory)
+ if (CommandLineOptions.Clo.MonomorphicArrays)
mapTypeSynonym = abstractedType;
else
mapTypeSynonym = new CtorType(Token.NoToken, synonymDecl, mapTypeParams);