diff options
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 1a2af93b..b765a1c3 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -698,6 +698,11 @@ namespace Microsoft.Boogie { }
else {
outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {
+ for (int i = 0; i < errors.Count; i++) {
+ errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
+ }
+ }
}
}
catch (VCGenException e) {
@@ -721,12 +726,6 @@ namespace Microsoft.Boogie { }
}
- if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen)) {
- for (int i = 0; i < errors.Count; i++) {
- errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
- }
- }
-
ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
if (CommandLineOptions.Clo.XmlSink != null) {
|