<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="">I’m not sure what you mean by letting Z3 manage memory. Unless something has changed significantly since I looked at the source, the Z3 C++ API simply wraps memory management functions from the lower-level Z3 C API using C++ objects. Since the constraint manager is using the C API, due to compatibility issues with RTTI and exceptions, it needs to call the appropriate memory management functions.<div class=""><br class=""></div><div class="">Likewise, I’m not sure what cache memory you’re referring to. There was some discussion of a SMT query cache in CSA, but I don’t believe that was ever implemented.<br class=""><div class=""><br class=""></div><div class="">Dominic<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 8, 2018, at 5:01 AM, 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="">Hello,<br class=""><br class=""></div>I looked at the references on this mail <a href="http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html" class="">http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html</a><span id="goog_332505968" class=""></span><span id="goog_332505969" class=""></span><span id="goog_332505958" class=""></span><span id="goog_332505959" class=""></span> and then looked at Z3ConstraintManager.cpp and I have some questions regarding the solver:<br class=""><br class=""></div>1) Right now we are not letting Z3 manage memory. Will it be a good idea to do that?<br class=""></div>2) Can we flush the cache memory in the destructor of <b class="">Z3Solver <a href="https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834" class="">https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834</a> </b>class?<br class=""><br class="">Thank you very much,<br class="">Ashish Kumar Gahlot<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>
_______________________________________________<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=""></div></div></body></html>