SMT solvers such as Z3 or Boolector use a complex set of heuristics to solve problems. However, this also makes predicting the performance of such a solver for a given problem very hard. My question is thus:
Is there a way to understand or gain insights into the performance of a SMT solver for a specific in the theory of quantifier-free bitvectors (QFBV)?
This also includes any visualization tools that would help to understand where the solver is "stuck" / does not make progress.
Understand in advance how different encodings of the same problem affect solver performance (the state of the art here can't be "just try a few different encodings and hope one is fast enough", right?)
If a given problem is not solveable by an SMT solver due to time constraints, find a way to express the problem differently so that it can be solved.
Avoid wasting time on domain-specific problem simplifications that won't affect solver performance at all or even negatively affect solver performance.
I tried to find research on this topic, but I have not been able to find much. I do not have much experience in the field of SAT/SMT solvers yet, so apologies if I have missed something.
SATzilla: predicts best performing solver based on features extracted from the problem using machine-learning techniques.
This applies only with SAT instead of SMT, and does not explain the reasons for solvers performance.
Z3 axiom profiler A visualization of Z3 instantiation graph and analysis of matching loops
Looks like this focuses only on the quantified theories.