<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class=""><div dir="ltr" style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><div class=""><div class=""><div class="gmail_extra"><div class="gmail_quote"><div class="">Option (ii) is something I personally really support and would like to see implemented in the analyzer. I was already thinking on this change earlier but did not seem easy to come up with a reliable heuristic for that. The aim is clear and great but how would you do it? Would you rate the possibilities based on the number of visits of the possible next analyzed blocks?<br class=""></div></div></div></div></div></div></div></blockquote><div><br class=""></div><div>In the queue we already have the counter on the number of times a given block was visited along the path;</div><div>The implementation I am currently playing with when comparing two paths would simply picks the one which has visited its CFGBlock less times along its path.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><div class=""><div class=""><div class="gmail_extra"><div class="gmail_quote"><div class=""><br class=""><br class=""></div><div class="">Thanks,<br class=""></div><div class="">Peter</div></div></div></div></div></div></div></blockquote></div><br class=""></body></html>