diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-10-02 22:27:35 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-10-02 22:27:35 +0100 |
| commit | 3297f35c08738cd95bd01c1f4ab1e8baadddf67e (patch) | |
| tree | 58adb68086eb78112a55005892fc53e749ff036d /Source/VCGeneration/VC.cs | |
| parent | 2a32d6e6a9b7e193c7a49893acc52397f1824d1d (diff) | |
small refactoring
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index f1c01758..85d0fb31 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1943,6 +1943,7 @@ namespace VC { Bpl.AssertCmd b = null;
if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvEntryAssert)
b = new Bpl.LoopInitAssertCmd(c.tok, Expr.True);
else
@@ -1956,6 +1957,7 @@ namespace VC { prefixOfPredicateCmdsInit.Add(b);
if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvMaintainedAssert)
b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);
else
|