Add wider floating-point regression coverage

[1sgtpepper]

Summary

Add behavior regressions for the wide fp.div and shared round paths in
Z3Prover/z3#10216.

The 24 independent wide cases keep one floating-point operand symbolic and constrain it
only with fp.eq, so the default QF_FP simplification path cannot fold fp.div before
fpa2bv. They cover exact normalization, directed underflow, ties, overflow endpoints,
ebits > sbits, and sbits == 2, with one expected result per case for precise failure
localization. Other regressions cover all rounding modes, special values, and the shared
rounder's wide shift-count paths. A dedicated FP(2,16) quotient fails if the shift cap
18 is represented as the wrapped four-bit value 2.

Source change: Z3Prover/z3#10216. This PR must merge after that source change and
remains draft until it lands.

Testing

• Exact paired fork validation at f42bacbf1 combines source head 51b80b21a with
  this test head 9593fb035: build/test
  (14/14 jobs) and OCaml bindings
  (2/2 jobs), both successful.
• The cap-width control
  changes only the shift-cap width and fails the dedicated FP(2,16) regression.
• The known-bad replay
  uses the unpatched PR base with this test head; all 24 isolated wide cases fail in
  each of its eight regression configurations. The cap-width control above isolates
  the exact cap regression at the same test head.
• No local Z3 build or solver executable was used; validation used the paired fork CI
  workflows.