1 files changed, 8 insertions, 0 deletions
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
+}