diff options
| author |  Rustan Leino <unknown> | 2015-01-27 20:38:55 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-01-27 20:38:55 -0800 |
| commit | 247a2d714e70f8f7be80307f53bdaf7d0033d54e (patch) | |
| tree | 3640cb296281da21d7e502124a55ed2329d161d0 /Test/dafny0/Basics.dfy.expect | |
| parent | cee001acf106fe23e7dd29df4c10c0a2a5293be4 (diff) | |
Assume type properties of values that are created by a havoc assignment. Such assignments are part of assign-such-that statements, and
thus this also fixes Issue 52.
Diffstat (limited to 'Test/dafny0/Basics.dfy.expect')
| -rw-r--r-- | Test/dafny0/Basics.dfy.expect | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Basics.dfy.expect b/Test/dafny0/Basics.dfy.expect index db074f4a..f28df20a 100644 --- a/Test/dafny0/Basics.dfy.expect +++ b/Test/dafny0/Basics.dfy.expect @@ -124,4 +124,4 @@ Execution trace: (0,0): anon4_Then
(0,0): anon3
-Dafny program verifier finished with 63 verified, 18 errors
+Dafny program verifier finished with 84 verified, 18 errors
|