diff options
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index c46a4e0b..0e962307 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -915,6 +915,14 @@ namespace VC #endregion
}
}
+ else if (task.type == CoverageGraphManager.Task.TaskType.REACHABLE)
+ {
+ if (done == 2) continue;
+ var node = task.queryNode;
+ // assert that any path must pass through this node
+ var expr = calls.getTrueExpr(node);
+ vState.checker.AddAxiom(expr);
+ }
else
{
Console.WriteLine("Ignoring task: " + task.ToString());
@@ -1016,7 +1024,7 @@ namespace VC allTrue = false;
}
}
- Debug.Assert(allTrue == true);
+
// Check
if (allFalse)
{
|