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/Provers/SMTLib/SMTLibLineariser.cs | 43 ++++++++++++++++++++++++++-----
 Source/VCExpr/VCExprASTVisitors.cs        | 35 ++++++++++++++++++++-----
 2 files changed, 65 insertions(+), 13 deletions(-)

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7c6a3a9a..5cd40896 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -211,24 +211,53 @@ namespace Microsoft.Boogie.SMTLib
 
     public bool Visit(VCExprNAry node, LineariserOptions options)
     {
-      //Contract.Requires(node != null);
-      //Contract.Requires(options != null);
-
       VCExprOp op = node.Op;
       Contract.Assert(op != null);
+      
+      if (op.Equals(VCExpressionGenerator.ImpliesOp))
+      {
+          // handle this operator without recursion
+          VCExprNAry iter = node;
+          List<VCExpr> conjuncts = new List<VCExpr>();
+          VCExpr next = null;
+          do
+          {
+              conjuncts.Add(iter[0]);
+              next = iter[1];
+              iter = next as VCExprNAry;
+              if (iter == null) break;
+          }
+          while (iter.Op.Equals(VCExpressionGenerator.ImpliesOp));
+
+          wr.Write("(=> ");
+          if (conjuncts.Count == 1)
+          {
+              Linearise(conjuncts[0], options);
+          }
+          else {
+            wr.Write("(and");
+            foreach (var e in conjuncts)
+            {
+                wr.Write(" ");
+                Linearise(e, options);
+            }
+            wr.Write(")");
+          }
+          wr.Write(" ");
+          Linearise(next, options);
+          wr.Write(")");
+          return true;
+      }
 
       if (op.Equals(VCExpressionGenerator.AndOp) ||
            op.Equals(VCExpressionGenerator.OrOp)) {
         // handle these operators without recursion
-
-        wr.Write("({0}",
-          op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");
+        wr.Write("({0}", op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");
         foreach (var ch in node.UniformArguments) {
           wr.Write("\n");
           Linearise(ch, options);
         }
         wr.Write(")");
-
         return true;
       }
 
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