[Condition Based Refinement] Runtime Improvements

[ebehner]

Proposal

The Condition Based refinement sometime takes 65% of the runtime (total time ~5 minutes) and sometimes only 11% (total time ~1minute) on the same sample. This should not happen. It seems that in the case this optimization need 65% of the time, that z3 does not fully simplify a condition, and we end up with computing 511 sub-expression. We should never compute this many sub-expression, but the stage should also be more independent of the success of the simplification of z3.

Approach

1. Make the stage less dependent on the simplification of z3
2. Make sure that we do not compute too many sub-expression, i.e., find a better way to only consider the sub-expression that make sense in the current content, and probably also not compute all at once, because we only use one, the first that fits.