For future dives into SMT, the following requirements are for SMT support:
- SMT queries should be stored for reproducibility.
- RunAllProves should not trigger the SMT solvers but should check SMT queries for regressions with the stored previous runs.
- The solver definitions (currently given as properties files) should be rewritten into KeY configuration files (json-like). This allows type-safety and more structured configuration.
- When structured concurrency is released from the Preview area, the SMT solver should use it for portfolio solving.
- CVC5 should receive test cases.
setup-smt should install Princess
setup-smt should install CVC4
For future dives into SMT, the following requirements are for SMT support:
setup-smtshould install Princesssetup-smtshould install CVC4