diff options
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.
|