KeY-2.12.3 (2024-09-08)

What's Changed

• Update LICENSE.TXT to reflect GPL-2.0-only by @FliegendeWurst in #3223
• Post-Release 2.12.0: Backport bug fixes into main by @wadoon in #3242
• Update BSH dependency of recoder by @wadoon in #3250
• Post-Release: Backport Deployment Changes to KeY by @wadoon in #3246
• Post-Release 2.12.0: Java and Version by @wadoon in #3241
• Applying Java 17 refactorings by @wadoon in #3252
• Fix dependency issue in SMT translation by @FliegendeWurst in #3275
• UI: avoid freeze when applying SMT results by @FliegendeWurst in #3255
• Stop automode or exit on SIGINT by @FliegendeWurst in #3249
• updating README.md by @mattulbrich in #3288
• Problem statements in KeY file can now also be a (semi-)sequent by @wadoon in #3283
• Further Refactorings for Java 17+ by @wadoon in #3264
• SMT: add Z3_QF variant by @FliegendeWurst in #3287
• Fix for issue #3158 by @unp1 in #3224
• Some general minor code quality improvements by @unp1 in #3293
• Update beanshell to 2.0b6 by @unp1 in #3294
• Backport of KEY-2.12.1 into main by @wadoon in #3296
• Fix wrong quicksave failed warning by @unp1 in #3298
• Fix for issue #3286: Parsing of rule display names that contain spaces in origin labels by @unp1 in #3306
• Restore TermImpl to package private and strengthen immutability of term and sorts by @unp1 in #3304
• Fix Issue #3186: Model method looses nullability modifiers by @unp1 in #3307
• Revert lazy term index updates by @unp1 in #3312
• Allow origin labels to be switched off completely by @unp1 in #3316
• Proof Slicing: make dependency tracking optional by @FliegendeWurst in #3309
• replace JSR305 annotations with JSpecify by @wadoon in #3290
• A heap indicator in KeY's status bar by @wadoon in #3325
• fix ClassCastException in LogicPrinter by @wadoon in #3326
• Fix JavaDoc errors by @unp1 in #3329
• Fix broken addLabel Method in TermBuilder by @Drodt in #3331
• Heap status extension: proper max. value of progress bar by @FliegendeWurst in #3332
• Fix all warnings reported by ./gradlew javadoc by @unp1 in #3330
• Method names should not be created via VariableRenamer by @unp1 in #3231
• Create a basic CONTRIBUTING.md by @FliegendeWurst in #3333
• Print real condition in if labels by @FliegendeWurst in #3222
• Fix consistency of proof status and tasktree icon by @unp1 in #3344
• Show notification after running macro by @FliegendeWurst in #3269
• Update to Java 21 Runtime for Testing by @wadoon in #3282
• Add help buttons to extension settings by @FliegendeWurst in #3348
• suggesting a pull-request-template. by @mattulbrich in #3018
• A new grammar for configuration by @wadoon in #3099
• Fix (for issue #3347) that node selection gets forgotten when switching between proofs by @unp1 in #3349
• Re-enable check for non-unique taclet names and remove two taclet duplicates by @unp1 in #3359
• Avoid name clashes in rule applyUpdateOnRigid by @tobias-rnh in #3355
• Handle bound variables in SMT unknown translation by @FliegendeWurst in #3263
• Fix update of proof tree in case of filter changes (fixes #3367) by @unp1 in #3368
• Configurable enabled keys for JML condition evaluation by @wadoon in #3373
• Get rid of experimental flag using more fine-grained flags by @wadoon in #3370
• ADTs for KeY by @wadoon in #3161
• Renovation: package.html to package-info.java by @wadoon in #3381
• Fix passing of warnings by @wadoon in #3302
• Proof caching: use dependency graph to increase hit rate by @FliegendeWurst in #3305
• Always sort extension actions in context submenus (+bugfix to allow disabling extensions) by @FliegendeWurst in #3392
• Update README.md (license date and Java version) by @WolframPfeifer in #3412
• Activate the OverloadedOperatorHandler.java for Sequence datatype by @wadoon in #3398
• Solved an issue with row/column numbers in JML Parser by @LennartKleinwort in #3419
• Fix error handling for unknown sorts by @MarcoScaletta in #3428
• Hackathon: error reporting by @FliegendeWurst in #3426
• Fix position info for equality expr errors by @FliegendeWurst in #3429
• Add ADT Destructors by @Drodt in #3420
• JML enabled keys indicator for the Status Line by @wadoon in #3374
• fixes #1533 by @JonasKlamroth in #3423
• Hackeython smt mod by @BookWood7th in #3418
• added checkbox to disable example loader directly in dialog by @JonasKlamroth in #3424
• Generalizing Logic Data Structures by @Drodt in #3357
• Fix startup crash if ~/.key/colors.json is not present by @FliegendeWurst in #3439
• fix smt solver downloader script by @wadoon in #3445
• Update broken link in README.md by @FliegendeWurst in #3444
• Update pull_request_template.md by @mattulbrich in #3446
• Immutable and valid JML set statement by @wadoon in #3400
• Combine equalsMod... methods by @tobias-rnh in #3386
• Introducing a new function symbol seqUpd by @mattulbrich in #3385
• Cleanup of declaration of taclet options by @WolframPfeifer in #3408
• Boyer Moore Majority Vote by @mattulbrich in #3454
• Hackeython/error reporting by @mattulbrich in #3432
• Nicer error message for parse errors by @FliegendeWurst in #3417
• Fixes a StackOverflow when pretty printing a taclet by @unp1 in #3453
• Fix newnames handling for new local vars by @FliegendeWurst in #3438
• Prevent Dependency PO generation for void methods by @Drodt in #3422
• Update dependabot configuration by @wadoon in #3447
• Add key features for the FM tutorial by @wadoon in #3460
• Fixed the path-to-smt-solver bug in windows by @vb213 in #3434
• Support for JML\TYPE by @flo2702 in #3465
• Basic Nullness Checker configuration by @wmdietl in #3183
• Nullness Type System activated for key.ncore by @wadoon in #3468
• Renovation of PO loading by @wadoon in #3379
• Fix checkstyle workflow by @Drodt in #3471
• Generalize ParsableVariable and Schemavariables by @Drodt in #3436
• Removal of JUnit4 by @wadoon in #3462
• Allow "\seq()" and "\locset()" in JML by @mattulbrich in #3476
• Introduce JML aliases of frame conditions for better tool compatibility by @mi-ki in #3365
• Fix loading of closed proofs (GUI threw error) by @unp1 in #3479
• Fix loading of taclet proof obligations (issue #3477) by @unp1 in #3481
• RuleCommand can now deal with rules that have schema variables for logical variables by @mattulbrich in #3482
• Additional rule for sequences: Swap of sequence is a permutation by @WolframPfeifer in #3485
• Hackeython unknown methods by @flo2702 in #3431
• Update Github Action for Gradle by @unp1 in #3480
• Fix overflow checking by @WolframPfeifer in #3353
• Fixed operator replacements in WD taclets after changes in PR #3436 by @mi-ki in #3484
• Realize generic navigation structure by @Drodt in #3472
• Overflow follow up fix by @WolframPfeifer in #3490
• More general equalsModProperty by @tobias-rnh in #3459
• saving proofs for sequent problems by @mattulbrich in #3496
• Map with new equalities by @tobias-rnh in #3486
• Remove Ctrl+C handling, see #3456 by @wadoon in #3499
• HacKeYthon: Improved Taclet Options by @tobias-rnh in #3433
• Fix for the LoopInvariantConfigurationDialog by @unp1 in #3377
• Revert "Fix CurrentGoalView highlights not being removed" by @mattulbrich in #3391
• Fix for #3501: Decrease log level of duplicate sort warnings by @WolframPfeifer in #3505
• Repairing the NonNull checker framework exception by @mattulbrich in #3507
• repairing heatmap updates for inner nodes by @mattulbrich in #3506
• Fix copyright notice by @flo2702 in #3508
• Fix for visual bug with overlapping/unreadable text in color settings by @WolframPfeifer in #3509
• Option to disable ProofTree tooltips, render them lazily by @WolframPfeifer in #3510

New Contributors

• @tobias-rnh made their first contribution in #3355
• @LennartKleinwort made their first contribution in #3419
• @MarcoScaletta made their first contribution in #3428
• @JonasKlamroth made their first contribution in #3423
• @BookWood7th made their first contribution in #3418
• @vb213 made their first contribution in #3434
• @wmdietl made their first contribution in #3183

Full Changelog: KeY-2.12.2...KEY-2.12.3