<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Ashish,<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 15, 2018, at 11:41 PM, Ashish Gahlot via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class=""><div class=""><div class=""><div class="">Hello all,<br class=""><br class=""></div>I was testing the performance of the z3 clang analyzer using the <a href="https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-industry-pattern/ofuf_1_true-unreach-call.c" class="">sv-benchmarks</a>. I experienced a huge performance issue in the analyzer[<a href="https://imgur.com/a/rEa1X" class="">image</a>].</div></div></div></div></div></blockquote><div><br class=""></div><div>Yes, hence the point of the GSOC project to only cross-check the counterexamples.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class=""><div class=""> Is there a way we can use something similar to <i class="">z3 -v<N> </i>when we run the analyzer to see where the z3 is getting stuck?<br class=""></div></div></div></div></div></blockquote><div><br class=""></div><div>No, there is no similar option for the analyzer.</div><div>I don’t think it would help you much though: most likely z3 is just performing a very large number of small queries at every step.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class=""><div class=""><br class=""></div>Another thing I wanted to ask is that does LLVM has a particular format in which a student has to submit his proposal?<br class=""></div></div></div></div></blockquote><div><br class=""></div><div>Probably the easiest is to search the list archives from the last year and to look for the previous analyzer GSoC applications.</div><div><br class=""></div><div>Regards,</div><div>George</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class=""><br class=""></div>Thank You,<br class=""></div>Ashish Kumar Gahlot <br clear="all" class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><div class=""><br class="">-- <br class=""><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><div dir="ltr" class=""><div class="">Ashish Kumar Gahlot</div><div class="">IV year, UG</div><div class="">Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div></div></div></div></div></div></div></div>
_______________________________________________<br class="">cfe-dev mailing list<br class=""><a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><br class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev<br class=""></div></blockquote></div><br class=""></body></html>