From 84121f913cd1e4f78847bb246c2a83ac116a1a1b Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sun, 27 Sep 2009 23:11:12 +0000
Subject: 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).

---
 Source/VCExpr/TypeErasurePremisses.ssc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source')

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 {
-- 
cgit v1.2.3