diff options
| author |  Bryan Parno <parno@microsoft.com> | 2015-10-19 22:53:41 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2015-10-19 22:53:41 -0700 |
| commit | 88f5ac86bda56381f81be032a0011e34aeca50a8 (patch) | |
| tree | 08cfa5f7b5d3896f9a8538291a9d584316b29daa /Test/dafny0/Fuel.dfy.expect | |
| parent | be08f2949d674bd757a804795de1dd37c95177f3 (diff) | |
Improve Dafny's ability to find fueled functions by checking the function itself,
as well as the signature and body of other functions.
Diffstat (limited to 'Test/dafny0/Fuel.dfy.expect')
| -rw-r--r-- | Test/dafny0/Fuel.dfy.expect | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index 90fe877d..0c128941 100644 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -91,5 +91,17 @@ Execution trace: Fuel.dfy(407,38): Error: assertion violation
Execution trace:
(0,0): anon0
+Fuel.dfy(435,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Fuel.dfy(436,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Fuel.dfy(457,23): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Fuel.dfy(458,23): Error: assertion violation
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 51 verified, 24 errors
+Dafny program verifier finished with 56 verified, 28 errors
|