patched two occurrences of StackOverflowException on benchmarks from IronClad

1 files changed, 36 insertions, 7 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;

       }