changes to support a configured errorLimit

1 files changed, 2 insertions, 9 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 5880eb16..e02f96d5 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1875,7 +1875,7 @@ namespace VC {
           }

       }

 

-    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int threadID = -1)

+    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int taskID = -1)

     {

     Contract.Requires(impl != null);

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -1946,7 +1946,7 @@ namespace VC {
               prefixOfPredicateCmdsInit.Add(b);

 

               if (CommandLineOptions.Clo.ConcurrentHoudini) {

-                if (CommandLineOptions.Clo.Cho[threadID].DisableLoopInvMaintainedAssert)

+                if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvMaintainedAssert)

                   b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

                 else

                   b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

@@ -1954,13 +1954,6 @@ namespace VC {
                 b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

               }

 

-              if (threadID >= 0 && CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)

-

-              if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)

-                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

-              else

-                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

-

               b.Attributes = c.Attributes; 

               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsMaintained.Add(b);