From e51b347511f11ea1bda810b843e5d61fdf088832 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 5 Jun 2010 02:00:33 +0000
Subject: Dafny: * Fixed bug in translation of well-formedness conditions *
 Added Test/dafny0/Celebrity.dfy * Added a harness to
 Test/vacid0/Composite.dfy

---
 Source/Dafny/Translator.ssc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source/Dafny')

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index eea9d91b..092ee146 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1303,7 +1303,8 @@ namespace Microsoft.Dafny {
           substMap.Add(p, ie);
           locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?
-          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(e.Args[i]));
+          Expression ee = e.Args[i];
+          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), (!)ee.Type, p.Type));
           builder.Add(cmd);
         }
         // check that the preconditions for the call hold
-- 
cgit v1.2.3