Improve qe-light elimination for BV vars constrained by constant (dis)equalities

[Copilot]

apply qe on a small BV existential formula could stall in practice, while the same shape is easy to simplify by case analysis on a small set of constant comparisons. This change teaches qe-light to recognize and eliminate that pattern directly.

• BV case-split expansion in qe-light

  • Added a bounded fallback in src/qe/lite/qe_lite_tactic.cpp for quantified BV variables that occur only in equalities with constants (including under negation).
  • For each such variable, enumerate:
    • each observed constant case, plus
    • one synthesized “default” value distinct from those constants.
  • Substitute each case into the body and disjoin the instantiated formulas, yielding a quantifier-free result when applicable.
  • Added hard bounds to prevent blowups:
    • per-variable case cap
    • total Cartesian-product case cap

• Integration point

  • Wired this BV expansion into the existing post-eq_der/FM quantifier reduction path, as a fallback alongside existing bounded-expansion logic.

• Regression coverage

  • Added a focused test in src/test/qe_arith.cpp using a minimized BV formula with the same structural pattern as the reported repro.
  • The test asserts:
    • quantifiers are eliminated by qe_lite
    • rewritten formula remains equivalent to the original quantified formula.

if (m_imp.try_expand_bounded_quantifier(q, result, expanded) ||
    m_imp.try_expand_bv_eq_quantifier(q, result, expanded)) {
    ...
}

[NikolajBjorner]

this fails fast instead of handling bit-vector variables that satisfy the conditions