summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r--Source/VCGeneration/VC.cs1
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 304130ef..9e8b2dc8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3021,6 +3021,7 @@ namespace VC {
errModel.Print(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
+
Hashtable traceNodes = new Hashtable();
foreach (string s in labels) {
Contract.Assert(s != null);