diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-03-02 12:06:22 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-03-02 12:06:22 -0800 |
| commit | b07e5b62739645a6a3a4018b41c0e8690f0e10ff (patch) | |
| tree | 8fa82e41be7a5623e9d6bf115b2046ea5ffdfd59 /Source/BoogieDriver | |
| parent | 90fb97596ed8068be758b5e9b6b7853fe0cb7cba (diff) | |
small fix for a bug I introduced during the refactoring of InferAndVerify
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) {
|