I've recently ported a project I'm working on to use Boolector as a alternate back-end. I'd like to know how to achieve the best performance for my workload.
At the moment the vast majority of my processing is done on quantifier free bit vectors only (QF_BV) and I generally need incremental use (doing a program synthesis problem with the usual "get one or more counter examples, add it/them to the model" flow - "CEGIS").
I tried two setups with Boolector - one was grabbing the SMTCOMP19 branch, and the other was default "master" branch.
The SMTCOMP19 branch was sensationally faster than master (about 11x faster on my problem), but is still somewhat slower than Yices.
Is the SMTCOMP19 branch the best starting point if I want to work on tuning my system with Boolector? Is there a planned release schedule?
Geoff.