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 ++++++++++++++++++++++++++-----
 1 file changed, 36 insertions(+), 7 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

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;
       }
 
-- 
cgit v1.2.3