3 files changed, 55 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bae3aa50..bcdb7126 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1311,3 +1311,14 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost
 -------------------- MultiSets.dfy --------------------
 
 Dafny program verifier finished with 22 verified, 0 errors
+
+-------------------- PredExpr.dfy --------------------
+PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative
+Execution trace:
+    (0,0): anon6_Else
+    (0,0): anon7_Else
+PredExpr.dfy(36,17): Error: condition in assert expression might not hold
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 7 verified, 2 errors
diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy
new file mode 100644
index 00000000..3499a01c
--- /dev/null
+++ b/Test/dafny0/PredExpr.dfy
@@ -0,0 +1,43 @@
+function Subonacci(n: nat): nat
+{
+  if 2 <= n then
+    // proving that this case is a nat requires more information,
+    // which is here supplied by an assume expression
+    assume Subonacci(n-2) <= Subonacci(n-1);
+    Subonacci(n-1) - Subonacci(n-2)
+  else
+    n
+}
+
+function F(n: int): nat
+{
+  Subonacci(assume 0 <= n; n) -
+  Subonacci(n)
+}
+
+function G(n: int, b: bool): nat
+{
+  if b then
+    Subonacci(assume 0 <= n; n)
+  else
+    Subonacci(n)  // error: n may not be a nat
+}
+
+ghost method M(m: nat, n: int)
+{
+  var k := F(m);
+  assert k == 0;
+  k := F(n);
+  assert k == 0;  // this is still known
+}
+
+method M0(j: int) returns (n: nat)
+{
+  n := assert 0 <= j; j;  // error: j may be negative
+}
+
+method M1(j: int) returns (n: nat)
+{
+  n := (assume 0 <= j; j) + (assert 0 <= j; j);
+  assert n == 2*j;
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c30ec3a5..32a60340 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
-            CallStmtTests.dfy MultiSets.dfy) do (
+            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f