diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-09 17:08:16 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-09 17:08:16 -0800 |
| commit | ea8f475d9f26ac46339bbaca436035b1b75c671d (patch) | |
| tree | 5619777f8702441b97f2c0032a9114fc5e1edb43 /Source/VCGeneration/StratifiedVC.cs | |
| parent | e29ca07f28a9c54c46f4c45a3d77c3cf7254d07f (diff) | |
Boogie: output number of proof obligations (asserts) along with timing information when using the /trace option
Diffstat (limited to 'Source/VCGeneration/StratifiedVC.cs')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index e1c5ce13..27237a51 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1692,7 +1692,9 @@ namespace VC }
}
if (toExpand.Count == 0) expand = false;
- else DoExpansion(incrementalSearch, toExpand, vState);
+ else {
+ DoExpansion(incrementalSearch, toExpand, vState);
+ }
}
}
#endregion
@@ -2402,14 +2404,13 @@ namespace VC static int newVarCnt = 0;
// Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
- private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState)
- {
- vState.expansionCount += candidates.Count;
+ private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState) {
+ vState.expansionCount += candidates.Count;
- if (incremental)
- DoExpansionAndPush(candidates, vState);
- else
- DoExpansionAndInline(candidates, vState);
+ if (incremental)
+ DoExpansionAndPush(candidates, vState);
+ else
+ DoExpansionAndInline(candidates, vState);
}
// Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
|