From 730df23957b61a2fbc8c5b9fa670adb6b18e523b Mon Sep 17 00:00:00 2001
From: Arne Keller <2012gdwu+github@posteo.de>
Date: Tue, 21 Nov 2023 17:23:40 +0100
Subject: [PATCH] Changelog: 2.12.2

Co-authored-by: Wolfram Pfeifer <94171076+WolframPfeifer@users.noreply.github.com>
---
 docs/changelog.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/docs/changelog.md b/docs/changelog.md
index cad9b43..ecc8657 100644
--- a/docs/changelog.md
+++ b/docs/changelog.md
@@ -1,5 +1,18 @@
 # Changelog
 
+## [2.12.2](https://github.com/KeYProject/key/releases/tag/KeY-2.12.2) (2023-11-10)
+This release contains bug fixes and performance enhancements.
+
+### Performance: 
+  - Z3 is now configurable to use the QF (quantifier-free) theory for problems without quantifiers.
+
+### Bug Fixes:
+  - The pretty printer no longer throws a ClassCastException when printing taclets using schema variables of an array type.
+  - Nullable and non-null modifiers attached to model methods are no longer lost.
+  - Term rule indices are now always up-to-date, preventing potential prover crashes.
+  - The counter-example dialog no longer freezes the GUI, if the example generation fails.
+  - The actual proof status and proof status icon in the task overview are now  consistent after pruning without requiring a manual refresh.
+
 ## [2.12.1](https://github.com/KeYProject/key/releases/tag/KEY-2.12.1) (2023-10-13)
 
 ### Bug fixes