Z3: clone the solver instead of adding constraints to a fresh instance #248
Conversation
|
Can you do some tests to check the performance impact on our existing angr/tests/perf tests (should be minimal) and also on some public solving-heavy tests - I would do test_tracer and then the wyvern example in angr-doc |
|
Also, if you have a workload which you feel like isn't represented by any of our standard perf tests, you can write one and submit a PR and we'll run it every night to check for regressions! |
|
I'd gladly do some more performance benchmarks. But before that could you help me understand why that one test fails? I don't understands what it is doing. |
|
It's a spurious failure. I've run it again and it's passed! |
|
OMG for five years we did not see the second comment in the original Z3 issue about |
|
This pull request has been marked as |
|
I'm going to merge this and fix any problems that come of it :) |
This results in increased incrementalism and thus speeds up further queries (See Z3Prover/z3#556). Leads to 10-25% reduction in execution time in my private benchmarks.