Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.

1 files changed, 3 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0e83f54a..41076a65 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -8693,7 +8693,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(codeContext != null);

         List<Expression> contextDecreases = codeContext.Decreases.Expressions;

         List<Expression> calleeDecreases = callee.Decreases.Expressions;

-        CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, etran.Old, builder, codeContext.InferredDecreases, null);

+        CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, tySubst, etran, etran.Old, builder, codeContext.InferredDecreases, null);

       }

 

       // Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.

@@ -8804,6 +8804,7 @@ namespace Microsoft.Dafny {
     void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Expression> calleeDecreases,

                               Bpl.Expr allowance,

                               Expression receiverReplacement, Dictionary<IVariable,Expression> substMap,

+                              Dictionary<TypeParameter, Type> typeMap,

                               ExpressionTranslator etranCurrent, ExpressionTranslator etranInitial, Bpl.StmtListBuilder builder, bool inferredDecreases, string hint) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(contextDecreases));

@@ -8835,7 +8836,7 @@ namespace Microsoft.Dafny {
         tok = new ForceCheckToken(tok);

       }

       for (int i = 0; i < N; i++) {

-        Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);

+        Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap, typeMap);

         Expression e1 = contextDecreases[i];

         if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {

           N = i;