diff options
| author |  Rustan Leino <unknown> | 2014-01-11 10:36:54 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-11 10:36:54 -0800 |
| commit | 59f0250f9b4cb78b65f48cfcbddfd22f5271e96d (patch) | |
| tree | 3b3072b7f5a58abaedce92282df62c3e96654b64 /Test | |
| parent | ad2d0b62367ee8c99f1b037190b2c29c4b7434a5 (diff) | |
| parent | 335ac08951e427500de34d55b14713cced6c12bd (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 13 |
2 files changed, 13 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 364e6c93..41cd8b02 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2083,7 +2083,7 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 46 verified, 8 errors
+Dafny program verifier finished with 49 verified, 8 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 684de262..0936176f 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -285,4 +285,15 @@ module StaticTest { {
g(y)
}
-}
\ No newline at end of file +
+ static predicate IsEven(x:int)
+
+ static function EvenDoubler(x:int) : int
+ requires IsEven(x);
+
+ // Should succeed thanks to auto-generated requirement of IsEven
+ static function {:autoReq} test(y:int) : int
+ {
+ EvenDoubler(y)
+ }
+}
|