BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)

BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)

Match:       `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`

Match:       `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`

Match:       `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`

On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
          | CVC4-base                              | CVC4-concatpullup-or                     |
BENCHMARK | SLVD   SAT   UNSAT   TO   MO   CPU[s]  | SLVD   SAT   UNSAT   TO  MO   CPU[s]  |
   totals | 38992 13844  25148  1082  28  984887.4 | 39028 13845  25183  1046 28  974819.1 |
```