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

3 files changed, 13 insertions, 3 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2758e189..bff09734 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/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));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 6b7a1079..a0ddd7f1 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1585,7 +1585,7 @@ Maps.dfy(126,13): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 30 verified, 2 errors

+Dafny program verifier finished with 32 verified, 2 errors

 

 -------------------- LiberalEquality.dfy --------------------

 LiberalEquality.dfy(18,14): Error: arguments must have the same type (got T and U)

diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy
index a49ac3c1..1c245952 100644
--- a/Test/dafny0/Maps.dfy
+++ b/Test/dafny0/Maps.dfy
@@ -180,3 +180,13 @@ method m14()
    assert u[1] == 1 && u[3] == 4;

    assert domain(u) == {0, 1, 3, 4};

 }

+

+class A { var x: int; }

+

+method m15(b: set<A>) 

+  requires forall a | a in b :: a != null;

+{

+  var m := map a | a in b :: a.x;

+  var aa := new A;

+  assert aa !in m;

+}
\ No newline at end of file