diff options
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 11 |
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);
|