summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2010-09-18 14:45:36 +0000
committerGravatar akashlal <unknown>2010-09-18 14:45:36 +0000
commit23bd0ad65b0b2a8bcea687e7b12047a6005d3889 (patch)
tree6b048fd5f51d532cf067b834e68d6e505bab757b /Source/VCGeneration/VC.cs
parentdbc59dc5f6dd703720df9815ed83158a351417fe (diff)
Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r--Source/VCGeneration/VC.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 31bcef54..775a04cc 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2636,7 +2636,7 @@ namespace VC {
// recursed on proc(id)
public int getRecursionBound(int id)
{
- int ret = 1;
+ int ret = 0;
var str = getProc(id);
while (candidateParent.ContainsKey(id))
{