<div dir="ltr"><div>Hello,<br><br></div>Thank you for the detailed explanation.<br><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <span dir="ltr"><<a href="mailto:dan@su-root.co.uk" target="_blank">dan@su-root.co.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
@Dominic: On a related note. If you remember, a while back we spoke<br>
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their<br>
performance characteristics and radically different (Z3_mk_solver()<br>
being much faster most of the time for us in KLEE [1]).<br>
I've just noticed that you're using `Z3_solver_push()` and<br>
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why<br>
you had performance regressions when you tried switching to<br>
`Z3_mk_solver()`. When you use Z3_solver_push(),<br>
Z3 switches to a slower incremental solver internally [2,3]. You might<br>
find that if you remove the pushes and pops and use `Z3_mk_solver()`<br>
that things work better.<br></blockquote><div> </div><div>I read the issue [2] and it explains that it when we use (push), z3 tries to<br></div><div>use the second solver. I think it would be a good idea to remove Solver.push()<br></div><div>from Z3ConstraintManager.<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
[1] <a href="https://github.com/Z3Prover/z3/issues/1035" rel="noreferrer" target="_blank">https://github.com/Z3Prover/<wbr>z3/issues/1035</a><br>
[2] <a href="https://github.com/Z3Prover/z3/issues/1459" rel="noreferrer" target="_blank">https://github.com/Z3Prover/<wbr>z3/issues/1459</a><br>
[3] <a href="https://github.com/Z3Prover/z3/issues/1053" rel="noreferrer" target="_blank">https://github.com/Z3Prover/<wbr>z3/issues/1053</a><br>
</blockquote></div><br></div><div class="gmail_extra">Sorry for a noob question but is it possible to test the changes that I make to <br></div><div class="gmail_extra">Z3ConstraintManager.cpp without having to compile the whole clang every time?<br><br>Thank you very much,<br>Ashish Kumar Gahlot</div><div class="gmail_extra"><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>