From b42d69a32e0e3a8132fd4b1288618fe4a7392eb6 Mon Sep 17 00:00:00 2001
From: Akash Lal <akashl@microsoft.com>
Date: Fri, 5 Jun 2015 10:09:41 +0530
Subject: Fix for SI: initialize extraRecBound

---
 Source/VCGeneration/StratifiedVC.cs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index da2c37c6..037fa2be 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -837,15 +837,7 @@ namespace VC {
     public StratifiedVCGen(bool usePrevCallTree, HashSet<string> prevCallTree, 
                            Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers) 
     : this(program, logFilePath, appendLogFile, checkers)
-    {
-      this.extraRecBound = new Dictionary<string, int>();
-      program.TopLevelDeclarations.OfType<Implementation>()
-          .Iter(impl => 
-              {
-                  var b = QKeyValue.FindIntAttribute(impl.Attributes, "SIextraRecBound", -1);
-                  if(b != -1) extraRecBound.Add(impl.Name, b);
-              });
-          
+    {          
       if (usePrevCallTree) {
         callTree = prevCallTree;
         PersistCallTree = true;
@@ -859,6 +851,14 @@ namespace VC {
       : base(program, logFilePath, appendLogFile, checkers, null) {
       PersistCallTree = false;
       procsThatReachedRecBound = new HashSet<string>();
+
+      extraRecBound = new Dictionary<string, int>();
+      program.TopLevelDeclarations.OfType<Implementation>()
+          .Iter(impl =>
+          {
+              var b = QKeyValue.FindIntAttribute(impl.Attributes, "SIextraRecBound", -1);
+              if (b != -1) extraRecBound.Add(impl.Name, b);
+          });
     }
 
     // Extra rec bound for procedures
-- 
cgit v1.2.3