2 files changed, 31 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bdbb8822..bae3aa50 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -133,8 +133,11 @@ Execution trace:
     (0,0): anon6_Else
     (0,0): anon7_Else
     (0,0): anon8_Then
+NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative
+Execution trace:
+    (0,0): anon3_Then
 
-Dafny program verifier finished with 12 verified, 8 errors
+Dafny program verifier finished with 15 verified, 9 errors
 
 -------------------- SmallTests.dfy --------------------
 SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 47bc22e1..0513591c 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -108,3 +108,30 @@ function Abs(x: int): nat
 {
   if 0 <= x then x else -x
 }
+
+// ----- Here are tests that the type of the result value of a function is known by the
+// ----- time the well-formedness of the function's specification is checked.
+
+function TakesANat(n: nat): bool
+{
+  n < 29
+}
+
+function Naturally(): nat
+  ensures TakesANat(Naturally());  // the wellformedness of this check requires 
+{
+  17
+}
+
+function Integrally_Bad(): int
+  ensures TakesANat(Integrally_Bad());  // error: well-formedness check fails
+{
+  17
+}
+
+function Integrally_Good(): int
+  ensures 0 <= Integrally_Good();
+  ensures TakesANat(Integrally_Good());  // here, the needed information follows from the preceding ensures clause
+{
+  17
+}