Fix intermittent key.core.testgen failures from SMT symbol-map race

[unp1]

Intended Change

key.core.testgen has been failing intermittently in CI for the last few weeks
(e.g. run 28220166551). All ~13 failures (TestCE.* with SolverException,
TestcaseGenerationE2ETest.arrayUtil) trace to a single root cause:
RuntimeException: Unknown operator: EQUALS … intSym.size=18 bvSym.size=34
raised during SMT term translation.

Root cause: the static SMT symbol tables in SMTTermMultOp (mirrored in
SMTTermBinOp) were lazily initialised by publishing an empty map to the
static field and only then populating it
(bvSymbols = new HashMap<>(); bvSymbols.put(...)), with non-volatile,
unsynchronised fields. With concurrent SMT solver threads, one thread can
observe a half-built map and miss EQUALS (which both maps actually contain),
producing the spurious error — a timing-dependent, intermittent failure.

This PR fixes the race and hardens the surrounding solver infrastructure:

• SMTTermMultOp / SMTTermBinOp: build the symbol tables eagerly and
  publish them as immutable maps (Map.copyOf) in private static final
  fields, removing the lazy-init window entirely.
• VersionChecker: the version probe gated on BufferedReader.ready(),
  which returns false whenever the solver's output is not yet buffered (a
  race under load) and then reported "no version". It now waits for the process
  to terminate before reading, raises the timeout to 10s, and returns null on
  error instead of throwing.
• SolverTypeImplementation: version support is now compared numerically
  rather than lexicographically (the old comparison sorted e.g. 4.13.0 before
  the configured minimum Z3 version 4.4.1).
• TestCommons: when the solver is not installed/usable, the test now skips
  via a JUnit assumption instead of silently returning a passing result. Genuine
  solver/translation errors are deliberately still surfaced as failures.
• tests.yml: pin setup-smt to z3Version: 4.13.0 so CI is reproducible.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code
• There are changes to the deployment/CI infrastructure (gradle, github, ...)

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: ran :key.core.testgen:test for TestCE
  and TestcaseGenerationE2ETest locally with Z3 4.15.4 — all pass (previously
  13 failed); key.core compiles and spotlessApply reports no changes.
• I have checked that runtime performance has not deteriorated: the symbol maps
  are now built once eagerly rather than lazily, so there is no per-call cost.

Additional information and contact(s)

PR created with AI tooling support.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[Drodt]

Thanks!