diff options
| author |  rustanleino <unknown> | 2009-09-27 23:11:12 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-09-27 23:11:12 +0000 |
| commit | 84121f913cd1e4f78847bb246c2a83ac116a1a1b (patch) | |
| tree | 4e2b02bef38ed0b879b223a4761c423255fd323d /Source/VCExpr | |
| parent | 62a881760f8db7256343500ebafda8c72f0ca927 (diff) | |
Use type-erased result type to make decision about whether or not to include antecedent in select-of-store axioms (fixing an error in my previous check-in).
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/TypeErasurePremisses.ssc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCExpr/TypeErasurePremisses.ssc b/Source/VCExpr/TypeErasurePremisses.ssc index 10fb1247..40c062e0 100644 --- a/Source/VCExpr/TypeErasurePremisses.ssc +++ b/Source/VCExpr/TypeErasurePremisses.ssc @@ -664,7 +664,7 @@ namespace Microsoft.Boogie.TypeErasure AxBuilderPremisses.Type2Term(mapResult, bindings.TypeVariableBindings));
VCExpr body;
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None ||
- !AxBuilder.U.Equals(mapResult))
+ !AxBuilder.U.Equals(((!)select.OutParams[0]).TypedIdent.Type))
{
body = Gen.Let(letBindings_Explicit, eq);
} else {
|