Recursive walking of Exprs doesn't play nice when the depth of the AST is high.

Reduce depth of AST whenever possible (e.g., use a binary tree instead of a
linear list of terms)

1 files changed, 4 insertions, 4 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index e4f63315..13ff6460 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -241,12 +241,12 @@ namespace VC {
     public void GenerateVC() {

       if (initialized) return;

       List<Variable> outputVariables = new List<Variable>();

-      Expr assertExpr = new LiteralExpr(Token.NoToken, true);

+      List<Expr> assertConjuncts = new List<Expr>();

       foreach (Variable v in impl.OutParams) {

         Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

         outputVariables.Add(c);

         Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

-        assertExpr = Expr.And(assertExpr, eqExpr);

+        assertConjuncts.Add(eqExpr);

       }

       foreach (IdentifierExpr e in impl.Proc.Modifies) {

         if (e.Decl == null) continue;

@@ -254,9 +254,9 @@ namespace VC {
         Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

         outputVariables.Add(c);

         Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

-        assertExpr = Expr.And(assertExpr, eqExpr);

+        assertConjuncts.Add(eqExpr);

       }

-      exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(assertExpr));

+      exitAssertCmd = new AssertCmd(Token.NoToken, Expr.Not(Expr.BinaryTreeAnd(assertConjuncts)));

 

       Program program = vcgen.program;

       ProverInterface proverInterface = vcgen.prover;