summaryrefslogtreecommitdiff
path: root/Source/Concurrency/YieldTypeChecker.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-02-18 17:16:02 -0800
committerGravatar qadeer <unknown>2014-02-18 17:16:02 -0800
commitd834836a1250a8964ce9d9b7ca50e673643a9eba (patch)
treec5bc39d3b59364cc534ea07c801d5f95ce683a5b /Source/Concurrency/YieldTypeChecker.cs
parentc0252c602f4e77efafa93f5ba51a704319fe61d7 (diff)
fixed a bug in the automaton construction labeling
Diffstat (limited to 'Source/Concurrency/YieldTypeChecker.cs')
-rw-r--r--Source/Concurrency/YieldTypeChecker.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 086e68fa..fd632994 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -277,7 +277,8 @@ namespace Microsoft.Boogie
}
else
{
- Debug.Assert(false);
+ Debug.Assert(parCallCmd.CallCmds.Count == 1);
+ edgeLabels[edge] = 'A';
}
}
}