diff options
| author |  Rustan Leino <unknown> | 2014-01-05 16:22:38 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-05 16:22:38 -0800 |
| commit | 621178a0da1fee756dcf6dd713c8ef5b14530800 (patch) | |
| tree | 4ddd0ef17a84aacc805b6c8ecbd053d9e198c27c /Test/dafny0/Answer | |
| parent | 9fcb57c00fd690da3a86dbc890bc32f6fc352079 (diff) | |
More thoroughly check for nested assume statements during compilation
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0ce33b47..472932c5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2327,7 +2327,7 @@ Dafny program verifier finished with 0 verified, 0 errors Dafny program verifier finished with 44 verified, 0 errors
Compiled assembly into Compilation.exe
-Dafny program verifier finished with 9 verified, 0 errors
+Dafny program verifier finished with 15 verified, 0 errors
Compilation error: Arbitrary type ('_module.MyType') cannot be compiled
Compilation error: Iterator _module.Iter has no body
Compilation error: Method _module._default.M has no body
@@ -2335,3 +2335,7 @@ Compilation error: Method _module._default.P has no body Compilation error: an assume statement cannot be compiled (line 8)
Compilation error: Function _module._default.F has no body
Compilation error: Function _module._default.H has no body
+Compilation error: an assume statement cannot be compiled (line 17)
+Compilation error: an assume statement cannot be compiled (line 20)
+Compilation error: an assume statement cannot be compiled (line 25)
+Compilation error: an assume statement cannot be compiled (line 34)
|