Support extractbits_exprt with non-constant index in SMT2 backend

[tautschnig]

When the index of extractbits_exprt is not a compile-time constant, the SMT extract operator (which requires constant indices) cannot be used directly. Instead, shift the source bitvector right by the non-constant index using logical_shift_right (bvlshr), then apply a constant extract from bit 0 to (result_width - 1).

If the index and source have different bit widths, the index is zero-extended or truncated to match the source width, as required by the SMT logical_shift_right operator.

Unit tests updated to verify both same-width and different-width non-constant index cases.

Remove the no-new-smt exclusion tag from six regression test descriptors that were blocked on non-constant extractbits support in the incremental SMT2 backend. Also promote Pointer28/test.desc from KNOWNBUG to CORE since the underlying issue is now fixed.

Fixes: #8065

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.