This is an expanded version of https://git.key-project.org/key/key/-/merge_requests/562.

Original description, modified with additional changes:

Saves the name of the SMT solver that was able to close a goal in the proof file (and take it into account when loading). Also saves the unsat core reported by the SMT solver (currently only enabled for Z3).

Why

When a goal is closed by applying an SMT solver result, at the moment the solver that was able find an unsat result is not saved in the proof. In the saved file, the corresponding line looks like this: (builtin "SMTRule") When the proof is reloaded, the SMT solvers are run again. However, when multiple solvers are installed, it is unclear, which of them is used. I think it depends on the current user settings, i.e. the file proofIndependentSettings.proofs in the .key folder, but I am not sure, as changing the key [SMTSettings]ActiveSolver did not produce reliable results on my machine.

Further Note

With this MR, when I load the proof key.ui/examples/heap/verifyThis17_1_PairInsertionSort/sort.proof.gz (which currently experiences a timeout on Jenkins, see !558), for replay the Z3 solver is selected instead of CVC5, which decreases the loading time from 15 minutes to under 10 minutes on my machine. So while not solving the root cause of the problem, it may also help with timeout.

Feature

• The name of the successful solver and the formulas in the unsat core are stored in the proof file, for example: (builtin "SMTRule" (ifInst "" (formula "7")) (ifInst "" (formula "3")) (ifInst "" (formula "2")) (ifInst "" (formula "1")) (solverType "Z3"))
• When reloading, a solver with the given name is searched for in the available solvers. If available, this one is taken. Otherwise the current default solver is used (Z3).
• If no solverType is specified (legacy proofs), the replay is tried with Z3. It probably has the highest chance to work, most likely the proof was originally done with Z3, since for a long time we only supported this solver.
• [x] There is a switch to completely disable SMT proof search during proof reloading (shows a warning).

Open and possible tasks for the future

• [ ] When multiple solvers are run, at least one of them has to return unsat, others may return unknown for the result to be applicable and close the goal. Currently, for saving one of the solvers that returned unsat is selected, but I do not know according to which criteria (probably the one that first appears in the solver union). For the future, the fastest one should be selected.
• [ ] In addition to saving the solver name, we could also save branch specific settings, for example the timeout or some specific options for the solvers (e.g., translation without type hierarchy).