<div dir="ltr">Hi,<div><br></div><div>Thanks again for the comments and explanations. I hope I've incorporated all of your advice, except for this one.</div><div><br></div><div>George: I've been thinking about what you wrote ("<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">unifying a place where the constraints are dropped, and adding a flag guarding that"</span>) </div><div>and I have to admit that I'm not sure I understand that precisely.</div><div><br></div><div>Constraints dropped before being added to the environment should mean that SValBuilder gave up while trying to construct a specific</div><div>symbolic expression from them (returned an UnknownVal), if I understand correctly. Now, the logic responsible for this seems pretty</div><div>much scattered around, so I thought maybe by unifying you mean creating a function like the constraint managers' canReasonAbout()?</div><div>Supposing that building more complex expressions (if such will be added) might be expensive, something like that could come handy in</div><div>controlling the level of detail. Did you mean something like that?</div><div><br></div><div>Thanks,</div><div>Réka</div><div><br></div><div><br><div class="gmail_extra"><br><div class="gmail_quote">2018-03-25 22:26 GMT+02:00 George Karpenkov <span dir="ltr"><<a href="mailto:ekarpenkov@apple.com" target="_blank">ekarpenkov@apple.com</a>></span>:<br><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">Hi Réka,<div><br></div><div>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>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="m_2379769367196519423HOEnZb"><font color="#888888"><div><br></div></font></span><div><span class="m_2379769367196519423HOEnZb"><font color="#888888">George</font></span><div><div class="m_2379769367196519423h5"><br><div><br><blockquote type="cite"><div>On Mar 24, 2018, at 1:52 PM, Réka Nikolett Kovács <<a href="mailto:rekanikolett@gmail.com" target="_blank">rekanikolett@gmail.com</a>> wrote:</div><br class="m_2379769367196519423m_3387306277682206925Apple-interchange-newline"><div><div dir="ltr"><div>Hi,</div><div><br></div><div>I'd like to add my own version of a Z3 integration proposal draft:</div><div><br></div><a href="https://docs.google.com/document/d/1Qpw_rQ8-JFJJtqyJz8YBqui-FNcBgJJvpLBvPcCzHV4/edit?usp=sharing" target="_blank">https://docs.google.com/docume<wbr>nt/d/1Qpw_rQ8-JFJJtqyJz8YBqui-<wbr>FNcBgJJvpLBvPcCzHV4/edit?usp=s<wbr>haring</a><br><div><br></div><div>Any feedback would be much appreciated.</div><div><br></div><div>Thanks,</div><div>Réka</div></div>
</div></blockquote></div><br></div></div></div></div></blockquote></div><br></div></div></div>