experiment with "symbolic branch prediction" to avoid solver calls?

[zapashcanon]

Something between concolic and symbolic execution.

This is similar to what is done in https://ieeexplore.ieee.org/abstract/document/10123579 but I'm not sure we need to use AI for this, we could try to re-use well known branch prediction techniques (see for instance https://danluu.com/branch-prediction/ which is a good introduction).

The idea would be to predict which branches are reachable instead of asking the solver (we should be able to make a guess quickly) and to only call the solver at the end of execution when we may have found a bug.