What's Changed Breaking Changes 🗲 Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522 Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529 Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618 Refactoring context menus of sequent views by @wadoon in https://github.com/KeYProject/key/pull/3641 AST for KeY Scripts by @wadoon in https://github.com/KeYProject/key/pull/3587 Higher Order Proof Scripts by @wadoon in https://github.com/KeYProject/key/pull/3654 Modularization: InfFlow and WD as separate modules by @wadoon in https://github.com/KeYProject/key/pull/3640 Make the context menu more flexibel and type safe. by @wadoon in https://github.com/KeYProject/key/pull/3785 Purge sort depending functions in favor of parametric functions by @Drodt in https://github.com/KeYProject/key/pull/3773 Exciting New Features 🎉 Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578 Renovation of the TestCase generation by @wadoon in https://github.com/KeYProject/key/pull/3388 Add Polymorphic Sorts and Functions by @Drodt in https://github.com/KeYProject/key/pull/3652 The Removal of Recoder by @wadoon in https://github.com/KeYProject/key/pull/3120 Proof Scripts in JML by @mattulbrich in https://github.com/KeYProject/key/pull/3657 Features Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537 highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573 Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495 Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594 SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592 Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514 Introducing some structure for model method bodies by @mattulbrich in https://github.com/KeYProject/key/pull/3571 Linearized symbolic execution in proof tree by @FliegendeWurst in https://github.com/KeYProject/key/pull/3237 KeY/JSON config for SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3597 Save proof independent settings, that are not used by the configuration by @PiIsRational in https://github.com/KeYProject/key/pull/3700 Send Feedback using Github issues by @wadoon in https://github.com/KeYProject/key/pull/3736 Pfeifer/proof mgmt includes fix by @WolframPfeifer in https://github.com/KeYProject/key/pull/3757 Add sort aliases by @Drodt in https://github.com/KeYProject/key/pull/3778 Give similar taclet names if taclet not found during proof loading by @wadoon in https://github.com/KeYProject/key/pull/3784 Add support for Annotation Processors in the Javac Extension by @PiIsRational in https://github.com/KeYProject/key/pull/3686 Options Panel in Load Dialog. Options in Recent Files by @wadoon in https://github.com/KeYProject/key/pull/3788 Add support for var variable declarations by @Drodt in https://github.com/KeYProject/key/pull/3821 Basic Theory of Sets by @WolframPfeifer in https://github.com/KeYProject/key/pull/3777 Collapsing proof search by @unp1 in https://github.com/KeYProject/key/pull/3825 Improvements for the Taclet Match Dialog by @unp1 in https://github.com/KeYProject/key/pull/3830 Allow realizing multiple cached branches at once by @FliegendeWurst in https://github.com/KeYProject/key/pull/3440 automode to choose from a dropdown list by @mattulbrich in https://github.com/KeYProject/key/pull/3857 Feature: Version-based Configuration Paths by @wadoon in https://github.com/KeYProject/key/pull/3888 Bug Fixes Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520 Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525 Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533 Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540 fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560 Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566 Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559 Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543 fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583 Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593 Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598 Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609 fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619 Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629 Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606 Fix NPE using KeY command line interface caused by Java NIO by @wadoon in https://github.com/KeYProject/key/pull/3643 FIX: URGENT: Changes in Gradle 9 results into non-execution of custom test tasks. by @wadoon in https://github.com/KeYProject/key/pull/3653 fix css for sequentview syntaxhighlightning by @wadoon in https://github.com/KeYProject/key/pull/3645 Allow true in more JML expressions by @mattulbrich in https://github.com/KeYProject/key/pull/3664 Fix NPE in dependency contract feature (caused by pulled out expression) by @unp1 in https://github.com/KeYProject/key/pull/3675 Fix Information Flow Proof Loading for KeY Jar File by @Drodt in https://github.com/KeYProject/key/pull/3678 Enable assertion for :key.ui:run by @wadoon in https://github.com/KeYProject/key/pull/3682 Fix proof task tree forced white background. by @wadoon in https://github.com/KeYProject/key/pull/3663 Fix deadlock when showing JML warnings dialog by @FliegendeWurst in https://github.com/KeYProject/key/pull/3692 Check for applicability of Antec-/SuccTaclets in Proof Replay by @Drodt in https://github.com/KeYProject/key/pull/3702 Return to Metal as default Look and Feel by @WolframPfeifer in https://github.com/KeYProject/key/pull/3658 fix #3721, getParent().toUri() requires absolute paths by @wadoon in https://github.com/KeYProject/key/pull/3722 Fix unbalanced block exception when pretty printing heap terms by @unp1 in https://github.com/KeYProject/key/pull/3726 Add reachable Java state properties to invariant for modified local variables (fixes #3728) by @unp1 in https://github.com/KeYProject/key/pull/3747 Fix for #3738: Fix SMT type axiomatisation for interfaces by @WolframPfeifer in https://github.com/KeYProject/key/pull/3749 Anonymize ghost variables in loop by @Drodt in https://github.com/KeYProject/key/pull/3729 Proof Management: Ignore internal contracts when calculating dependency state (fixes #3745) by @WolframPfeifer in https://github.com/KeYProject/key/pull/3748 Fix for #3683: Hiding package prefixes in sequent view by @WolframPfeifer in https://github.com/KeYProject/key/pull/3684 Taclet definition added to problemHeader by @wadoon in https://github.com/KeYProject/key/pull/3733 put CachingExtension into the correct service file. by @wadoon in https://github.com/KeYProject/key/pull/3782 move Taclet options of WD from key.core to key.core.wd by @wadoon in https://github.com/KeYProject/key/pull/3783 Allow KeY to start even in case of unreadable recent files by @unp1 in https://github.com/KeYProject/key/pull/3790 ProofManagement extension: Iterative NodeIntermediateWalker to avoid stack overflows by @WolframPfeifer in https://github.com/KeYProject/key/pull/3793 Dependency Contract: Ignore all term labels when searching for base term by @FliegendeWurst in https://github.com/KeYProject/key/pull/3776 Alternative for #3393: Fix slicing bug related to Evaluate Query by @WolframPfeifer in https://github.com/KeYProject/key/pull/3794 Fix field names in Isabelle translation by @unp1 in https://github.com/KeYProject/key/pull/3795 Enable KeY to distinguish between classes of same name in different packages by @unp1 in https://github.com/KeYProject/key/pull/3805 Improve behavior in case of not found methods by @unp1 in https://github.com/KeYProject/key/pull/3806 Fix naming and renaming issues by @unp1 in https://github.com/KeYProject/key/pull/3804 Fix Path bug by @wadoon in https://github.com/KeYProject/key/pull/3810 Fix bug in ProofManagementDialog by @unp1 in https://github.com/KeYProject/key/pull/3812 Fix 'choose contract' in parser by @Drodt in https://github.com/KeYProject/key/pull/3840 Fixes for minor regressions on main by @unp1 in https://github.com/KeYProject/key/pull/3844 Make new name creation only dependent on goal namespaces not on global counter by @unp1 in https://github.com/KeYProject/key/pull/3848 Fix per-proof memory leak: clear JavaParserFacade cache on dispose by @unp1 in https://github.com/KeYProject/key/pull/3854 Make cross-platform path/URI/charset handling in load/save more robust by @unp1 in https://github.com/KeYProject/key/pull/3860 Fix "Rule of same name exists already" error after pruning (rare but occuring cases after mass pruning with try-closeable-goals) by @unp1 in https://github.com/KeYProject/key/pull/3850 Fix most-recent file not set after loading recent-files list (#3711) by @unp1 in https://github.com/KeYProject/key/pull/3866 Reject generic sorts at user-input boundaries: \problem, JML, taclet instantiation (#3409) by @unp1 in https://github.com/KeYProject/key/pull/3869 Fix fast-click auto-mode crash: overlapping runs + proof breaking proof listeners by @unp1 in https://github.com/KeYProject/key/pull/3880 Fix NPE when copying a namespace set with a root sub-namespace by @unp1 in https://github.com/KeYProject/key/pull/3881 Follow-up fixes for cost-reuse: remove unsound static caches by @unp1 in https://github.com/KeYProject/key/pull/3873 Implement \real literals (#3570); fix LogicPrinter.quickPrintSemisequent (#243) by @unp1 in https://github.com/KeYProject/key/pull/3865 Fix changing Taclet Options via the GUI (and more) + TimSort source files added as examples by @unp1 in https://github.com/KeYProject/key/pull/3889 Fix two soundness gaps in select/permission taclets by @unp1 in https://github.com/KeYProject/key/pull/3891 Cost-Reuse: Fix latent classification bugs and code cleanup by @unp1 in https://github.com/KeYProject/key/pull/3890 Fix GUI crashes when no proof is loaded, and remove dead MainWindowTabbedPane by @unp1 in https://github.com/KeYProject/key/pull/3892 Fix for DepthFirstGoalChooser: Keep enabled sibling goals on a split by @unp1 in https://github.com/KeYProject/key/pull/3886 Fix finalFields default in FinalHeapResolution.isFinalEnabled by @unp1 in https://github.com/KeYProject/key/pull/3895 Dependencies Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516 Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517 Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527 Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526 Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531 Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536 Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577 Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581 Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589 Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596 Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603 Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617 Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627 Bump the gradle-deps group with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3646 Bump the gradle-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3649 Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3655 Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3656 Bump gradle/actions from 4 to 5 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3667 Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3666 Bump the gradle-deps group with 9 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3679 Bump actions/upload-artifact from 4 to 5 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3680 Bump actions/checkout from 5 to 6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3694 Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3695 Bump the gradle-deps group with 4 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3704 Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3705 Bump the gradle-deps group with 4 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3712 Bump the gradle-deps group with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3731 Bump actions/upload-artifact from 6 to 7 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3752 Bump the gradle-deps group across 1 directory with 9 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3756 Bump the github-actions-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3798 Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3797 Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3807 Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3815 Bump the gradle-deps group across 1 directory with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3818 Bump actions/checkout from 6 to 7 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3871 Bump the gradle-deps group across 1 directory with 9 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3872 Migrate to Gradle Version Catalog by @wadoon in https://github.com/KeYProject/key/pull/3894 Other Changes Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523 fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519 RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521 Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528 Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488 Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535 Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558 repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556 Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562 Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550 Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574 Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569 Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579 Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600 Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607 Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610 Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612 Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613 Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615 Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605 Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616 Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608 Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599 Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624 Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626 Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622 Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551 Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628 Reduce raw usage of classes by @Drodt in https://github.com/KeYProject/key/pull/3634 Fix multiple SLF4J providers by @BookWood7th in https://github.com/KeYProject/key/pull/3639 Indent switch expressions by @Drodt in https://github.com/KeYProject/key/pull/3636 Translation of bitwise operators by @ChristianHein in https://github.com/KeYProject/key/pull/3172 Throw an error when encountering an undefined rule set by @Drodt in https://github.com/KeYProject/key/pull/3644 Preparation for generalizing rule indexing by @unp1 in https://github.com/KeYProject/key/pull/3620 Improvements for AbbrevMap by @wadoon in https://github.com/KeYProject/key/pull/3647 small fixes to datatype handling by @mattulbrich in https://github.com/KeYProject/key/pull/3661 Improve error message in headless mode by @fynngodau in https://github.com/KeYProject/key/pull/3685 Set version to 2.13.0-dev by @wadoon in https://github.com/KeYProject/key/pull/3689 Generate easier POs for non-trivial diverges clauses by @Drodt in https://github.com/KeYProject/key/pull/3430 (Re-)activating an ancient rule for the treatment of exactInstance of null by @mattulbrich in https://github.com/KeYProject/key/pull/3706 Migrating to central portal from OSSRH, due to OSSRH shutdown in summer'25 by @wadoon in https://github.com/KeYProject/key/pull/3604 Fix nullchecker by @Drodt in https://github.com/KeYProject/key/pull/3732 Fix NPE in proof tree when using global filters by @flo2702 in https://github.com/KeYProject/key/pull/3755 Refixing #3721: Starting KeY UI with local files by @mattulbrich in https://github.com/KeYProject/key/pull/3754 Modularity for Proof Strategies by @Drodt in https://github.com/KeYProject/key/pull/3650 Update and fix Broad Release Tests by @wadoon in https://github.com/KeYProject/key/pull/3703 Support for TextBlockLiterals by @wadoon in https://github.com/KeYProject/key/pull/3796 Record support by transformation by @wadoon in https://github.com/KeYProject/key/pull/3758 Suppression of log for non-failing test classes by @wadoon in https://github.com/KeYProject/key/pull/3746 Update function explanations to new syntax by @Drodt in https://github.com/KeYProject/key/pull/3811 Update Gradle version to 9.5 and deprecated method replacements by @unp1 in https://github.com/KeYProject/key/pull/3813 Remove codecov from CI by @wadoon in https://github.com/KeYProject/key/pull/3802 Artifacts are now on mvn central by @wadoon in https://github.com/KeYProject/key/pull/3820 Local performance improvements by @unp1 in https://github.com/KeYProject/key/pull/3824 Improvements of Error Messages and Accurracy of Error Position Reporting by @unp1 in https://github.com/KeYProject/key/pull/3826 Improve Update Simplification for Long Programs by @unp1 in https://github.com/KeYProject/key/pull/3828 Deployment to Maven Central SNAPSHOT by @wadoon in https://github.com/KeYProject/key/pull/3819 Optimize NonDuplicateEqApp-features by @unp1 in https://github.com/KeYProject/key/pull/3829 Modularize KeY Grammar by @Drodt in https://github.com/KeYProject/key/pull/3822 Make semicolon after rule optional by @Drodt in https://github.com/KeYProject/key/pull/3832 Support co- and contravariant sorts by @Drodt in https://github.com/KeYProject/key/pull/3841 Fix gradle task dependencies by @wadoon in https://github.com/KeYProject/key/pull/3853 Remaining Changes for the KeY JSON-RPC API by @wadoon in https://github.com/KeYProject/key/pull/3849 Revert "Create temporary PR body file" by @wadoon in https://github.com/KeYProject/key/pull/3852 Taclet match dialog: collapse big matched terms; add an editor for SV fields by @unp1 in https://github.com/KeYProject/key/pull/3855 Fix newline escape for Windows by @Drodt in https://github.com/KeYProject/key/pull/3856 Further improvements on error message reporting by @unp1 in https://github.com/KeYProject/key/pull/3859 Performance (5/5): operator-indexed parking of assumes-incomplete rule-app bases by @unp1 in https://github.com/KeYProject/key/pull/3838 Performance (3/5): skip the checkPrefix prefix-walk when no transformer is present by @unp1 in https://github.com/KeYProject/key/pull/3836 Performance (2/5): cut proof-search allocations + release the parser DFA cache by @unp1 in https://github.com/KeYProject/key/pull/3835 Performance (1/5): Matching can now partially evaluate taclets by @unp1 in https://github.com/KeYProject/key/pull/3831 Performance (4/5): reuse rule-app cost across re-expansion (+ age as a cost term) by @unp1 in https://github.com/KeYProject/key/pull/3837 LogicPrinter: reduce per-subterm overhead and harden against unbalanced blocks by @unp1 in https://github.com/KeYProject/key/pull/3861 Make proof-tree painting cheap on large proofs by @unp1 in https://github.com/KeYProject/key/pull/3863 Fix intermittent key.core.testgen failures from SMT symbol-map race by @unp1 in https://github.com/KeYProject/key/pull/3862 Regression tests for resolved parser/JML issues (#1119, #1536); pin #329 by @unp1 in https://github.com/KeYProject/key/pull/3868 MetaSpace for documentation and origin by @wadoon in https://github.com/KeYProject/key/pull/3787 Update the InfoTree component by @wadoon in https://github.com/KeYProject/key/pull/3786 Report missing \endmodality at the modality opening; move source-location classes to ncore (#3867) by @unp1 in https://github.com/KeYProject/key/pull/3870 Better ImmutableList by @wadoon in https://github.com/KeYProject/key/pull/3816 Taclet match dialog: readable \assumes candidates and smarter window placement by @unp1 in https://github.com/KeYProject/key/pull/3882 Performance Series 2 (1/5): Faster cost computation by skipping an unnecessary proof-history walk by @unp1 in https://github.com/KeYProject/key/pull/3874 Performance Series 2 (2/5): Faster term equality modulo renaming via a hash pre-filter by @unp1 in https://github.com/KeYProject/key/pull/3875 Performance Series 2 (3/5): Incremental taclet re-indexing for a single added taclet by @unp1 in https://github.com/KeYProject/key/pull/3876 New Contributors @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558 @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568 @fynngodau made their first contribution in https://github.com/KeYProject/key/pull/3685 @PiIsRational made their first contribution in https://github.com/KeYProject/key/pull/3700 Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly