diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-05-21 19:04:09 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-05-21 19:04:09 -0700 |
| commit | e7422dc4757674758684c0e48f160eb37f42386a (patch) | |
| tree | 9798a99bd5fef7b3fd3fc1f0411cee4bdf719d57 /Source/Dafny/Compiler.cs | |
| parent | 9f87e7b7121a8003ae863dbe55b32a4118c578a3 (diff) | |
Allow more tail calls, on account of considering non-loop aggregate statements with only ghost sub-statements to be ghost
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 1aebf057..502f7f8a 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -998,6 +998,7 @@ namespace Microsoft.Dafny { Contract.Requires(stmt != null);
if (stmt.IsGhost) {
CheckHasNoAssumes(stmt);
+ Indent(indent); wr.WriteLine("{ }");
return;
}
|