diff --git a/CHANGELOG b/CHANGELOG
index 4052fe87941..ba9ceda5549 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,96 @@
+5.7
+===
+
+* General: All tools now support the same set of --*-check options.
+* General: Added --conversion-check to catch type casts that cause loss of
+  information. Previously --(un)signed-overflow-check would report these.
+* CBMC: New option --symex-coverage-report to produce a Cobertura-compatible
+  statement- and branch coverage report.
+* CBMC/Java: New options --java-max-vla-length, --java-unwind-enum-static,
+  --java-cp-include-files, --lazy-methods.
+* GOTO-INSTRUMENT: Static loop unwinding via --unwind or via new options
+  --unwindset, --unwindset-file, --unwinding-assertions, --partial-loops,
+  --continue-as-loops, --log
+* GOTO-INSTRUMENT: New option --slice-global-inits
+* GOTO-INSTRUMENT: Inlining via --inline, --partial-inline, --function-inline,
+  --no-caching
+* GOTO-INSTRUMENT: New options --remove-function-pointers, --model-argc-argv,
+  --show-threaded
+* GOTO-CC: Additional drop-in replacement support for bcc, as, as86
+* GOTO-CC: GCC-style error/warning messages
+* GOTO-CC: New options --native-compiler and --native-linker to select the
+  compiler/linker to be used when building combined native/goto object files.
+
+
+5.6
+===
+
+Bugfixes in the C, C++, Java front-ends.
+
+
+5.5
+===
+
+This is a major release, with significant changes. The option
+--all-properties is now the default; to restore the previous behaviour,
+use --stop-on-fail. The primary area of attention was again the Java
+front-end. We have furthermore added test-suite generation for branch
+coverage, location coverage, condition coverage, decision coverage and
+MC/DC.
+
+
+5.4
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+area of attention was again the Java front-end. We have also updated to
+Minisat 2.2.1.
+
+
+5.3
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+area of attention is the Java front-end.
+
+
+5.2
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+areas of attention are the full slicer, the Java frontend, test suite
+generation and support for the Glucose solver.
+
+
+5.1
+===
+
+This is a minor release, focused primarily on maintenance. Support for solving
+floating-point problems using for SMT-LIB2 solvers without support for the
+floating-point theory has been added.
+
+
+5.0
+===
+
+This is a major release, focused primarily on performance improvements.
+Furthermore, the support for the floating-point theory for SMT-LIB2 has been
+improved substantially. This release breaks compatibility with the goto-binary
+format used by earlier releases; i.e., you will need to rebuild your
+goto-binaries.
+
+
+4.9
+===
+
+This release is primarily for maintenance purposes and does not add any major
+new features. The support for SMT-LIB2 solvers has been improved substantially.
+
+
+4.8
+===
+
+
 4.7
 ===