diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java
index f3554d78..093b0098 100644
--- a/prism/src/prism/NondetModel.java
+++ b/prism/src/prism/NondetModel.java
@@ -321,6 +321,7 @@ public class NondetModel implements Model
 			}
 			log.println();
 			log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
+			log.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n");
 			log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
 			log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes, ");
 			log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars()+getNumDDNondetVars()) + " minterms\n");
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index 92468747..ec97baf2 100644
--- a/prism/src/prism/ProbModel.java
+++ b/prism/src/prism/ProbModel.java
@@ -274,6 +274,7 @@ public class ProbModel implements Model
 			}
 			log.println();
 			log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
+			log.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n");
 			log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
 		}
 		for (i = 0; i < numRewardStructs; i++) {
diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java
index cc12d951..b589fd69 100644
--- a/prism/src/prism/StochModel.java
+++ b/prism/src/prism/StochModel.java
@@ -274,6 +274,7 @@ public class StochModel implements Model
 			}
 			log.println();
 			log.print("Rate matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
+			log.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n");
 			log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
 		}