
<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 Réka,<div class=""><br class=""></div><div class="">Looks good overall!</div><div class=""><br class=""></div><div class="">There are two more items which could be included as super-stretch-goals: they would be very important for adoption of the project,</div><div class="">but fall far out of scope of the GSoC:</div><div class=""><br class=""></div><div class="">1) Packaging. This would be a huge barrier for adopting any Z3 work by existing analyzer users,</div><div class="">but maybe we can think about a few vectors where we could make the adoption easier.</div><div class="">E.g. how difficult would it be to add a dependency from the Debian package? Or from homebrew?</div><div class=""><br class=""></div><div class="">2) Stability. Z3 can segfault, bringing the entire analysis down.</div><div class="">The only way to address this I can think of would be running the solver out-of-process, communicating e.g. via SMT-LIB.</div><div class="">But that would considerably complicate the architecture and debugging, and I’m not sure the trade-offs are worth it.</div><div class=""><br class=""></div><div class="">George<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 26, 2018, at 8:05 AM, Réka Nikolett Kovács <<a href="mailto:rekanikolett@gmail.com" class="">rekanikolett@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class=""><div class="">Hi George and Artem,<br class=""><br class=""></div>Thanks for all your valuable comments!<br class="">I'll try to address all of them in a couple of hours.<br class=""><br class=""></div>Réka<br class=""><br class=""><br class=""><div class=""><div class=""><div class=""><div class="gmail_extra"><br class=""><div class="gmail_quote">2018-03-25 22:26 GMT+02:00 George Karpenkov <span dir="ltr" class=""><<a href="mailto:ekarpenkov@apple.com" target="_blank" class="">ekarpenkov@apple.com</a>></span>:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space" class="">Hi Réka,<div class=""><br class=""></div><div class="">Great! I think it would be beneficial to add an example where the “complex” constraint is dropped before even being added to the environment,</div><div class="">and add a stretch goal of fixing those (e.g. by unifying a place where the constraints are dropped, and adding a flag guarding that).</div><span class="HOEnZb"><font color="#888888" class=""><div class=""><br class=""></div></font></span><div class=""><span class="HOEnZb"><font color="#888888" class="">George</font></span><div class=""><div class="h5"><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Mar 24, 2018, at 1:52 PM, Réka Nikolett Kovács <<a href="mailto:rekanikolett@gmail.com" target="_blank" class="">rekanikolett@gmail.com</a>> wrote:</div><br class="m_-1783377539538339630Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hi,</div><div class=""><br class=""></div><div class="">I'd like to add my own version of a Z3 integration proposal draft:</div><div class=""><br class=""></div><a href="https://docs.google.com/document/d/1Qpw_rQ8-JFJJtqyJz8YBqui-FNcBgJJvpLBvPcCzHV4/edit?usp=sharing" target="_blank" class="">https://docs.google.com/<wbr class="">document/d/1Qpw_rQ8-<wbr class="">JFJJtqyJz8YBqui-<wbr class="">FNcBgJJvpLBvPcCzHV4/edit?usp=<wbr class="">sharing</a><br class=""><div class=""><br class=""></div><div class="">Any feedback would be much appreciated.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Réka</div></div>

</div></blockquote></div><br class=""></div></div></div></div></blockquote></div><br class=""></div></div></div></div></div>

</div></blockquote></div><br class=""></div></body></html>