Open LeventErkok opened 5 years ago
@NikolajBjorner
This benchmark has gotten a lot worse, sometime today. Now it doesn't complete even after running for 10 minutes. It's rather disconcerting as it used to be a mere 10 seconds but now seems to run forever.
smt.auto_config=false smt.relevancy=0 works much better on this.
Indeed it does much better! 25s on my machine now. Thanks!
I'm closing this ticket; but feel free to reopen if necessary.
I get "unknown" wtih some random seeds or internal code variants, not sure why. Overall, it could be that we just need to change the auto-config for this class to avoid relevancy which is both overhead and hides potentially useful lemmas. @nunoplopes - can you try relevancy=0?
I see a ~7% speedup with my custom solver stack and a slight reduction of timeouts. So, from this quick round of benchmarks, /me likes it!
FYI I'm trying now with relevancy=2 but auto_config=false to see if there's any difference.
Ok, I run my BV benchmarks with relevancy=2 and auto_config=false and got very similar results. So it seems the speedup is coming from somewhere else..
another example where smtfd smokes other approaches
The below benchmark has started exhibiting extremely terrible performance. I'm not exactly sure when this started, unfortunately. However, I do know that using z3 that I built on Jun 26th of 2018, it can be solved in about 10 seconds:
Unfortunately, a fresh build of z3 takes 22 times more, about 3 minutes and 42 seconds:
(Generated models are the same; so at least there's no soundness concern.)
Here's the benchmark: