Status of doomed program points

Nov 20, 2013 at 2:48 AM
What is the current status of the doomed program points (/vc:doomed)? I am wondering if the implementation is close to the one described in the FMSD'10 paper and just needs a few bug fixes, or needs more effort?

When I run the examples in Test\doomed\, Boogie seems to crash (when performing /debug):

System.InvalidOperationException was unhandled by user code
Message=Collection was modified; enumeration operation may not execute.
   at System.Collections.Generic.Dictionary`2.Enumerator.MoveNext()
   at VC.DCGen.GenerateReachabilityPredicates(Implementation impl) in e:\boogie_codeplex\Source\Doomed\VCDoomed.cs:line 676
   at VC.DCGen.Transform4DoomedCheck(Implementation impl) in e:\boogie_codeplex\Source\Doomed\VCDoomed.cs:line 737