<div dir="ltr"><div><div><div><div>Hello all,<br><br></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">sv-benchmarks</a>. I experienced a huge performance issue in the analyzer[<a href="https://imgur.com/a/rEa1X">image</a>]. Is there a way we can use something similar to <i>z3 -v<N> </i>when we run the analyzer to see where the z3 is getting stuck?<br><br></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><br></div>Thank You,<br></div>Ashish Kumar Gahlot <br clear="all"><div><div><div><div><div><div><div><br>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>Ashish Kumar Gahlot</div><div>IV year, UG</div><div>Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div></div></div></div></div></div></div></div>