<div dir="ltr">
<span></span>
<table cellspacing="0" border="0" style="font-family:"Liberation Sans";font-size:x-small">
<colgroup width="106"></colgroup>
<colgroup width="85"></colgroup>
<colgroup width="211"></colgroup>
<colgroup width="215"></colgroup>
<colgroup width="212"></colgroup>
<colgroup width="47"></colgroup>
<colgroup width="31"></colgroup>
<colgroup width="98"></colgroup>
<tbody style="font-family:"Liberation Sans";font-size:x-small"><tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Total Time</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">time.analyzer.time.sys (s) (mean)</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">time.analyzer.time.user (s) (mean)</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">time.analyzer.time.wall (s) (mean)</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Reported bugs</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Tmux</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">99.2</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.076</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">27.253</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.656</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">32</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Tmux + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">152.88</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.074</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">56.251</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">11.505</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">32</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">154.11%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">97.37%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">206.40%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">150.27%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Redis</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">173.69</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.057</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.083</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.271</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">146</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Redis + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">193.43</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.057</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.621</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.728</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">140</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">111.37%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">100.00%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">107.60%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">106.29%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">OpenSSL</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">264.93</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.042</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.31</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.412</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">204</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">OpenSSL + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">213.53</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.035</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.099</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.152</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">204</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">80.60%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">83.33%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">93.63%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">92.38%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Twin</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">143.17</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.067</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.593</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.696</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">138</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Twin + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">133.83</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.06</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.79</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.882</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">138</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">93.48%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">89.55%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">102.99%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">102.78%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Git + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">333.9</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.075</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.52</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.67</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">96</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Git + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">289.59</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.062</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.924</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.023</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">90</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">86.73%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">82.67%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">93.00%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">92.54%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Postgresql</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">889.35</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.079</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.482</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.631</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">676</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Postgresql + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">902.86</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.077</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">9.694</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">9.863</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">676</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">101.52%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">97.47%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">114.29%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">114.27%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Sqlite3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">1206.3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.262</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">368.446</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">370.786</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">200</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Sqlite3 + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">1260.85</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.43</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">407.763</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">409.688</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">199</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">104.52%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">164.12%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">110.67%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">110.49%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">1</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Average</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">104.62%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">102.07%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">118.37%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">109.86%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
</tbody></table>
<br></div><div class="gmail_extra"><br><div class="gmail_quote">2018-05-24 15:11 GMT+01:00 Mikhail Ramalho <span dir="ltr"><<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div>This is my first report to the community, comparing the results with and without the Z3 refutation when analyzing a number of projects.</div><div><br></div><div>~</div><div><br></div><div>First of all, I'd like to thank Réka Kovács as the first version of the refutation using Z3 was created by her (<a href="https://reviews.llvm.org/D45517" target="_blank">https://reviews.llvm.org/<wbr>D45517</a>)! Thank you very much!</div><div><br></div><div>After applying patch D45517, you can use the refutation check by using -analyzer-config crosscheck-with-z3=true. Obviously, you need a version of clang built with Z3.</div><div><br></div><div>~</div><div><br></div><div>I'm currently analyzing 7 C projects (unfortunately, there's a bug preventing us from analyzing FFmpeg):</div><div><br></div><div>1. Tmux</div><div>2. Redis </div><div>3. OpenSSL</div><div>4. Twin</div><div>5. Git</div><div>6. Postgresql</div><div>7. Sqlite3</div><div><br></div><div>In short, the refutation check slows down the verification by ~20%. It removed 6 FPs from Redis, 6 FPs from git and 1 FP from Sqlite3 (FP means false positive). Surprisingly enough, some analysis were faster with the crosscheck, but I'm not sure why (maybe ccache?).</div><div><br></div><div>Attached is a spreadsheet (report1.ods) with some number (total time, average time per check, # of reported bugs) and a txt with all the raw data from the analysis (raw.txt). I'll add these data to google drive for the next report.</div><div><br></div><div>In order to generate the raw data, you need to use a version of clang with assertions enabled, call scan-build.py with '-analyzer-config serialize-stats=true' and you need to apply patch <a href="https://reviews.llvm.org/D43134" target="_blank">https://reviews.llvm.<wbr>org/D43134</a>.</div><div><br></div><div>Thank you very much,</div><div><br></div></div><div class="gmail_extra"><div><div class="gmail-h5"><br><div class="gmail_quote">2018-05-01 15:27 GMT+01:00 Mikhail Ramalho <span dir="ltr"><<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hello all,<div><br></div><div>My proposal for GSoC 2018 [0] about Bug Validation in the Clang Static Analyzer using the Z3 SMT Solver was accepted.</div><div><br></div><div>I'll work with George Karpenkov to improve the bug reports that the static analyzer produces by reducing the number of false bugs.</div><div><br></div><div>Thank you,</div><div><br></div><div>[0] <a href="https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq_TY4AGjIpPu1VPkmO-g" target="_blank">https://docs.google.com/do<wbr>cument/d/1-zNSv0l4WyoxYpJUAw8L<wbr>FnQq_TY4AGjIpPu1VPkmO-g</a><span class="gmail-m_5428437582812369831gmail-HOEnZb"><font color="#888888"><br clear="all"><div><br></div>-- <br><div class="gmail-m_5428437582812369831gmail-m_1835488271327190244m_-1529477061806271292gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</font></span></div></div>
</blockquote></div><br><br clear="all"><div><br></div></div></div><span class="gmail-HOEnZb"><font color="#888888">-- <br><div class="gmail-m_5428437582812369831gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</font></span></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div>