diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt
index 1547e431..5f975436 100644
--- a/prism/CHANGELOG.txt
+++ b/prism/CHANGELOG.txt
@@ -1,19 +1,46 @@
 This file contains details of the changes in each new version of PRISM.
 
-Recent changes: (up to svn rev 10893)
-
-* Timeout feature (-timeout switch)
-* Built-in support for Nailgun client/server
-* Allow -exportpropaut to export DA in HOA format (-exportpropaut:hoa da.hoa)
-* Debugging options: -dddebug and -ddtrace command-line switches
-* Allow -javamaxmem switch for GUI as well as command line
-* Better error handling when CUDD runs out of memory
+Recent changes: (up to svn rev 12001)
+
+New model checking functionality:
+- expected reward to satisfy a co-safe LTL formula (all engines)
+- expected total reward (R[C] operator) for CTMCs
+- CTL model checking in the explicit engine
+- non-probabilistic LTL model checking in the explicit engine
+- instantaneous reward computation (Rmax/min[I=x]) in the explicit engine
+- DTMC transient probability computation for the explicit engine
+
+Imports and exports:
+- model import from explicit files for the explicit engine (-import... switches)
+- import of state rewards during explicit model import (symbolic engines)
+- export of models to .dot format via the -exportmodel switch
+- export of property automata to HOA format (-exportpropaut:hoa da.hoa)
+- export of state rewards from explicit engine
+
+Miscellaneous:
+- built-in support for Nailgun client/server
+- new timeout feature (-timeout switch)
+- performance improvements in explicit engine
+- GUI also supports -javamaxmem switch to set Java memory
+- better error handling when CUDD runs out of memory
+- various bug fixes and performance improvements
+
+Features for developers:
+- new ModelGenerator interface for specifying models programmatically
+- extensions to test mode: complex expressions for RESULT specifications
+- prism-auto: new options (--show-warnings, --nailgun, --ngprism), multiple -x switches
+- DD debugging options: -dddebug and -ddtrace switches, improved ref count debugging
+- code base now allows/assumes Java 8
+
+
+
+
+
+
 * Partial support for multi-objective queries expressed as Boolean expressions
 * Allow <<>> and [[]] operators for MDP (only * or empty), all engines
-* Model checking of expected reward to satisfy a co-safe LTL formula, all engines
-* Performance improvements in explicit engine
-* prism-auto: new options (--show-warnings, --nailgun, --ngprism), multiple -x switches
-* Bug fixes
+
+
 
 -----------------------------------------------------------------------------
 Version 4.3.1 (first released 26/5/2015)
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 1b12e702..4f455250 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -2306,6 +2306,7 @@ public class PrismCL implements PrismModelListener
 		mainLog.println("-test .......................... Enable \"test\" mode");
 		mainLog.println("-testall ....................... Enable \"test\" mode, but don't exit on error");
 		mainLog.println("-javamaxmem .................... Set the maximum heap size for Java, e.g. 500m, 4g [default: 1g]");
+		mainLog.println("-timeout <n> ................... Exit after a time-out of <n> seconds if not already terminated");
 		mainLog.println();
 		mainLog.println("IMPORT OPTIONS:");
 		mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language");