diff options
| author |  Rustan Leino <unknown> | 2015-10-02 18:56:13 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-10-02 18:56:13 -0700 |
| commit | cfe05df94a5ccb6025c94bd21b09bfc1240de756 (patch) | |
| tree | 94585c6f9e721829719472e5802367562c0e9f11 /Source | |
| parent | 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 (diff) | |
Made /rewriteFocalPredicates:1 the default
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 2d8756d2..b61ba555 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny public bool CountVerificationErrors = true; public bool Optimize = false; public bool AutoTriggers = false;
- public bool RewriteFocalPredicates = false;
+ public bool RewriteFocalPredicates = true;
public bool PrintTooltips = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; @@ -379,9 +379,9 @@ namespace Microsoft.Dafny 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. /rewriteFocalPredicates:<n> - 0 (default) - Don't rewrite predicates in the body of prefix lemmas. - 1 - In the body of prefix lemmas, rewrite any use of a focal predicate - P to P#[_k-1]. + 0 - Don't rewrite predicates in the body of prefix lemmas. + 1 (default) - In the body of prefix lemmas, rewrite any use of a focal predicate + P to P#[_k-1]. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires |