Dafny: fixed translation bug in maps with objects in the domain, added test case

1 files changed, 2 insertions, 2 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 2758e189..bff09734 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -6087,10 +6087,10 @@ namespace Microsoft.Dafny {
           var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));

           translator.otherTmpVarCount++;

 

-          Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, yVar), bv.Type, this);

           Bpl.Expr unboxy = !ModeledAsBoxType(bv.Type) ? translator.FunctionCall(e.tok, BuiltinFunction.Unbox, translator.TrType(bv.Type), new Bpl.IdentifierExpr(expr.tok, yVar))

             : (Bpl.Expr)(new Bpl.IdentifierExpr(expr.tok, yVar));

-

+          Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, unboxy, bv.Type, this);

+          

 

           Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();

           subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));