2 files changed, 9 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bcdb7126..3198df33 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1321,4 +1321,4 @@ 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
+Dafny program verifier finished with 9 verified, 2 errors
diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy
index 3499a01c..740c2308 100644
--- a/Test/dafny0/PredExpr.dfy
+++ b/Test/dafny0/PredExpr.dfy
@@ -41,3 +41,11 @@ method M1(j: int) returns (n: nat)
   n := (assume 0 <= j; j) + (assert 0 <= j; j);
   assert n == 2*j;
 }
+
+function SpecOnly(): bool { true }
+
+function method FuncMeth(): int {
+  assert SpecOnly();  // this call is allowed, because the .Guard of a
+                      // PredicateExpr is not included in compilation
+  15
+}