1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linear procedure call

2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation.  These are set just before inlining is called and now I reset them to null afterwards to help garbage collection.
3. Clear live variables right after passification again to help garbage collection.

1 files changed, 6 insertions, 4 deletions

diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 289dff87..52681162 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -47,6 +47,10 @@ namespace Microsoft.Boogie.VCExprAST
       return this;

     }

 

+	public virtual LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {

+      return this;

+    }

+    

     private static readonly List<VCExprVar!>! EmptyList = new List<VCExprVar!>();

 

     public bool NativeBv { get {

@@ -477,10 +481,8 @@ namespace Microsoft.Boogie.VCExprAST
 

       wr.Write("(LET (");

 

-      LineariserOptions! optionsWithVars = options;

-      foreach (VCExprVar! var in node.BoundVars)

-        optionsWithVars = optionsWithVars.AddLetVariable(var);

-

+      LineariserOptions! optionsWithVars = options.AddLetVariables(node.BoundVars);

+	  

       string s = "(";

       foreach (VCExprLetBinding! b in node) {

         wr.Write(s);