diff options
| author |  leino <unknown> | 2015-05-07 08:55:44 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-07 08:55:44 -0700 |
| commit | cafbf508ea7aa6f337140293105060393ccb11f5 (patch) | |
| tree | 5885eeda1ea285e3b043da8ffa8d7633d0a6fc0d /Test/dafny0/InductivePredicates.dfy.expect | |
| parent | f98a30f1ad7c441d8ef9e6e5740752723a43413a (diff) | |
Added "inductive lemma" methods
Diffstat (limited to 'Test/dafny0/InductivePredicates.dfy.expect')
| -rw-r--r-- | Test/dafny0/InductivePredicates.dfy.expect | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect index c0feb7dd..a57b7d70 100644 --- a/Test/dafny0/InductivePredicates.dfy.expect +++ b/Test/dafny0/InductivePredicates.dfy.expect @@ -1,5 +1,9 @@ -InductivePredicates.dfy(51,11): Error: assertion violation
+InductivePredicates.dfy(71,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+InductivePredicates.dfy(83,11): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 13 verified, 1 error
+Dafny program verifier finished with 18 verified, 2 errors
|