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 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