Use a custom Github action for setting up the SMT solvers

[wadoon]

Intended Change

Exchange of the dlsmt.sh scripts in favor of a real Github action that uses Github's API for setting up the SMT solvers.

This action is self-written and available here: https://github.com/KeYProject/setup-smt

Benefit: The pipeline becomes OS-independent and now we can run macOS and windows pipelines with SMT solvers. This PR also enables SMT solvers on windows unit-test pipelines!

On the road: Fixes for double artifact names on 8our broad release tests](https://github.com/KeYProject/key/actions/workflows/tests_winmac.yml).

Type of pull request

• No code changed.
• There are changes to the deployment/CI infrastructure (github)

  • board release tests needs to be triggered manually

    broad release test is currently broken as it uses --release 21 on a JRE 17.

Ensuring quality

• I have tested the feature as follows: CI

---

I currently have only added z3 and CVC5 to setup-smt as these were also in dlsmt.sh. Looking at java-smt3 the following exists:

• Bitwuzla
• Boolector
• CVC4
• CVC5
• MathSAT5
• OpenSMT
• OptiMathSAT
• Princess
• SMTInterpol
• Yices2
• Z3

Please add a PR at keyproject/setup-smt if some of these are required.

[wadoon]

Strange: Unit tests succeed on windows, but not on Linux.

Error on Linux is:

unit-tests (ubuntu-latest, 21)
The runner has received a shutdown signal. This can happen when the runner service is stopped, or a manually started runner is canceled.

This happens after 25 min. The Windows run needs 45 min. to complete.

@WolframPfeifer @mattulbrich We might hit a memory boundary limit here. Do we have experience with z3 4.14 and cvc5 1.2.1? I would remove the later one from the pipeline for testing.

[wadoon]

From KaKeY:

• #testDiv5 and '#testDiv6' are deactivated as their runtime hit the timeout (total of 10 min. runtime). They are probably the cause of the unexpected shutdown problems on Linux runners.

Issues: #3575

[mattulbrich]

We agreed to keep the two cases with shorter timeout. Since the timeout can unfortunately not be set individually for test cases but is driven by a special settings class, the overhead is not worth it and we keep them deactivated.