From fa6b47445e52ef471560deb44e62965982daa63a Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 16 Dec 2014 22:40:16 -0800
Subject: patched two occurrences of StackOverflowException on benchmarks from
 IronClad

---
 Source/VCExpr/VCExprASTVisitors.cs | 35 +++++++++++++++++++++++++++++------
 1 file changed, 29 insertions(+), 6 deletions(-)

(limited to 'Source/VCExpr/VCExprASTVisitors.cs')

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 02220057..c9d4f1c3 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -288,14 +288,15 @@ namespace Microsoft.Boogie.VCExprAST {
            node.Op == VCExpressionGenerator.ImpliesOp)) {
         Contract.Assert(node.Op != null);
         VCExprOp op = node.Op;
-
-        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
-        enumerator.MoveNext();  // skip the node itself
-
+        HashSet<VCExprOp> ops = new HashSet<VCExprOp>();
+        ops.Add(VCExpressionGenerator.AndOp);
+        ops.Add(VCExpressionGenerator.OrOp);
+        ops.Add(VCExpressionGenerator.ImpliesOp);
+        IEnumerator enumerator = new VCExprNAryMultiUniformOpEnumerator(node, ops);
         while (enumerator.MoveNext()) {
-          VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current);
+          VCExpr expr = cce.NonNull((VCExpr)enumerator.Current);
           VCExprNAry naryExpr = expr as VCExprNAry;
-          if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+          if (naryExpr == null || !ops.Contains(naryExpr.Op)) {
             expr.Accept(this, arg);
           } else {
             StandardResult(expr, arg);
@@ -433,6 +434,28 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
+  public class VCExprNAryMultiUniformOpEnumerator : VCExprNAryEnumerator
+  {
+      private readonly HashSet<VCExprOp> Ops;
+      [ContractInvariantMethod]
+      void ObjectInvariant()
+      {
+          Contract.Invariant(Ops != null);
+      }
+
+      public VCExprNAryMultiUniformOpEnumerator(VCExprNAry completeExpr, HashSet<VCExprOp> ops)
+          : base(completeExpr)
+      {
+          Contract.Requires(completeExpr != null);
+
+          this.Ops = ops;
+      }
+      protected override bool Descend(VCExprNAry expr)
+      {
+          return Ops.Contains(expr.Op) && expr.TypeParamArity == 0;
+      }
+  }
+
   //////////////////////////////////////////////////////////////////////////////
   // Visitor that knows about the variables bound at each location in a VCExpr
 
-- 
cgit v1.2.3