4 files changed, 30 insertions, 6 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1069f419..d4c97f0f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -646,6 +646,9 @@ axiom (forall b: BoxType, h: HeapType, t: BoxType ::
 axiom (forall b: BoxType, h: HeapType ::
   { GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) }
   GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h));
+axiom (forall dt: DatatypeType, h: HeapType ::
+  { GenericAlloc($Box(dt), h) }
+  GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h));
 // ==> GenericAlloc
 axiom (forall b: bool, h: HeapType ::
   $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 8d472098..7013a7ee 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1803,11 +1803,9 @@ namespace Microsoft.Dafny {
         } else {
           args.Add(formal);
         }
-        if (lits == null) {  // TODO(rustan): don't we need well-typedness conjuncts even when literal are involved?
-          // add well-typedness conjunct to antecedent
-          Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);
-          if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
-        }
+        // add well-typedness conjunct to antecedent
+        Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);
+        if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
       }
 
       Bpl.Expr funcAppl;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 29f7b8cc..5297d132 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2047,8 +2047,14 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 4 errors
 
 -------------------- Computations.dfy --------------------
+Computations.dfy(163,13): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Computations.dfy(168,13): Error: assertion violation
+Execution trace:
+    (0,0): anon0
 
-Dafny program verifier finished with 46 verified, 0 errors
+Dafny program verifier finished with 49 verified, 2 errors
 
 -------------------- ComputationsNeg.dfy --------------------
 ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index 641b8207..4b975559 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -150,3 +150,20 @@ ghost method copt_test()
   ensures copt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);
 {
 }
+
+// The following is a test that well-typedness antecednets are included in the literal axioms
+static function StaticFact(n: nat): nat
+  ensures 0 < StaticFact(n);
+{
+  if n == 0 then 1 else n * StaticFact(n - 1)
+}
+static method test_StaticFact()
+{
+  assert StaticFact(0) == 1;
+  assert 42 != 42;  // error:  this should fail
+} 
+method test_fact()
+{
+  assert fact(0) == 1;
+  assert 42 != 42;  // error:  this should fail
+}