diff --git a/prism/src/dd/dd_info.cc b/prism/src/dd/dd_info.cc
index c5a7df9b..3dc4e3c3 100644
--- a/prism/src/dd/dd_info.cc
+++ b/prism/src/dd/dd_info.cc
@@ -176,7 +176,7 @@ bool and_numbers)
 	Cudd_Ref(dd);
 	tmp = dd;
 	// Check the min (will use at end)
-	min = Cudd_V(Cudd_addFindMin(ddman, dd));
+	min = Cudd_V(Cudd_addFindMin(ddman, tmp));
 	// Loop through terminals in descending order
 	while (tmp != Cudd_ReadMinusInfinity(ddman)) {
 		// Find next (max) terminal and display
@@ -195,7 +195,7 @@ bool and_numbers)
 	Cudd_RecursiveDeref(ddman, tmp);
 	// Finally, print if there are (and possibly how many) minus infinities
 	if (and_numbers) {
-		if (count < pow(2, num_vars)) fprintf(dd_out, "-inf (%.0f)", pow(2, num_vars) - count);
+		if (count < (1<<num_vars)) fprintf(dd_out, "-inf (%.0f)", pow(2, num_vars) - count);
 	} else {
 		if (min == -HUGE_VAL) fprintf(dd_out, "-inf");
 	}
diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java
index 889807c7..0bcc6528 100644
--- a/prism/src/prism/Model.java
+++ b/prism/src/prism/Model.java
@@ -96,7 +96,8 @@ public interface Model
 	void fixDeadlocks();
 	void printTrans();
 	void printTrans01();
-	void printTransInfo(PrismLog log);
+	public void printTransInfo(PrismLog log);
+	public void printTransInfo(PrismLog log, boolean extra);
 	void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException;
 	String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException;
 	String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException;
diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java
index 7b836884..7b47b49f 100644
--- a/prism/src/prism/NondetModel.java
+++ b/prism/src/prism/NondetModel.java
@@ -287,7 +287,8 @@ public class NondetModel implements Model
 //		JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE);
 	}
 	
-	public void printTransInfo(PrismLog log)
+	public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
+	public void printTransInfo(PrismLog log, boolean extra)
 	{
 		int i;
 		
@@ -302,10 +303,13 @@ public class NondetModel implements Model
 		log.print(JDD.GetNumTerminals(trans) + " terminal), ");
 		log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, ");
 		log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c/" + getNumDDNondetVars() + "nd\n");
+		if (extra) log.println("DD var names: " + getDDVarNames());
+		if (extra) log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
 		
-		//log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
+		if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
 		
-		//log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes\n");
+		if (extra) log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes, ");
+		if (extra) log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars()+getNumDDNondetVars()) + " minterms\n");
 		
 		for (i = 0; i < numRewardStructs; i++) {
 			if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
@@ -313,12 +317,14 @@ public class NondetModel implements Model
 				log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes (");
 				log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), ");
 				log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n");
+				if (extra) log.print("State rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n");
 			}
 			if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) {
 				log.print("Transition rewards ("+i+"): ");
 				log.print(JDD.GetNumNodes(transRewards[i]) + " nodes (");
 				log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), ");
 				log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n");
+				if (extra) log.print("Transition rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n");
 			}
 		}
 	}
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index e6667f3a..78508f7b 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -60,6 +60,7 @@ public class PrismCL
 	private boolean exportordered = true;
 	private boolean simulate = false;
 	private boolean simpath = false;
+	private boolean extraDDInfo = false;
 	private int typeOverride = 0;
 	
 	// property info
@@ -557,7 +558,7 @@ public class PrismCL
 				// otherwise print error and bail out
 				else {
 					mainLog.println();
-					model.printTransInfo(mainLog);
+					model.printTransInfo(mainLog, extraDDInfo);
 					mainLog.print("\nError: Model contains " + states.size() + " deadlock states");
 					if (!verbose && states.size() > 10) {
 						mainLog.print(".\nThe first 10 deadlock states are displayed below. To view them all use the -v switch.\n");
@@ -575,7 +576,7 @@ public class PrismCL
 		
 		// print more model info
 		mainLog.println();
-		model.printTransInfo(mainLog);
+		model.printTransInfo(mainLog, extraDDInfo);
 	}
 
 	// do any exporting requested
@@ -1156,6 +1157,10 @@ public class PrismCL
 					prism.setVerbose(true);
 					verbose = true;
 				}
+				// extra dd info on
+				else if (sw.equals("extraddinfo")) {
+					extraDDInfo = true;
+				}
 				// precomputation algs off
 				else if (sw.equals("nopre")) {
 					prism.setPrecomp(false);
@@ -1485,6 +1490,7 @@ public class PrismCL
 		mainLog.println("-maxiters <n> .................. Set max number of iterations [default 10000]");
 		mainLog.println();
 		mainLog.println("-verbose (or -v) ............... Verbose mode: print out state lists and probability vectors");
+		mainLog.println("-extraddinfo ................... Display extra info about some (MT)BDDs");
 		mainLog.println("-nopre ......................... Skip precomputation algorithms");
 		mainLog.println("-fair .......................... Use fairness (when model checking PCTL on MDPs)");
 		mainLog.println("-nofair ........................ Don't use fairness (when model checking PCTL on MDPs) [default]");
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index 39235844..f61a9b18 100644
--- a/prism/src/prism/ProbModel.java
+++ b/prism/src/prism/ProbModel.java
@@ -248,7 +248,8 @@ public class ProbModel implements Model
 //		JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE);
 	}
 	
-	public void printTransInfo(PrismLog log)
+	public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
+	public void printTransInfo(PrismLog log, boolean extra)
 	{
 		int i;
 		
@@ -262,8 +263,10 @@ public class ProbModel implements Model
 		log.print(JDD.GetNumTerminals(trans) + " terminal), ");
 		log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, ");
 		log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n");
+		if (extra) log.println("DD var names: " + getDDVarNames());
+		if (extra) log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
 		
-		//log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
+		if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
 		
 		for (i = 0; i < numRewardStructs; i++) {
 			if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
@@ -271,12 +274,14 @@ public class ProbModel implements Model
 				log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes (");
 				log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), ");
 				log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n");
+				if (extra) log.print("State rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n");
 			}
 			if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) {
 				log.print("Transition rewards ("+i+"): ");
 				log.print(JDD.GetNumNodes(transRewards[i]) + " nodes (");
 				log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), ");
 				log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n");
+				if (extra) log.print("Transition rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n");
 			}
 		}
 	}
diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java
index 4dd709d9..7fcd5169 100644
--- a/prism/src/prism/StochModel.java
+++ b/prism/src/prism/StochModel.java
@@ -248,7 +248,8 @@ public class StochModel implements Model
 //		JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE);
 	}
 	
-	public void printTransInfo(PrismLog log)
+	public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
+	public void printTransInfo(PrismLog log, boolean extra)
 	{
 		int i;
 		
@@ -262,8 +263,10 @@ public class StochModel implements Model
 		log.print(JDD.GetNumTerminals(trans) + " terminal), ");
 		log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, ");
 		log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n");
+		if (extra) log.println("DD var names: " + getDDVarNames());
+		if (extra) log.print("Rate matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
 		
-		//log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
+		if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
 		
 		for (i = 0; i < numRewardStructs; i++) {
 			if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
@@ -271,12 +274,14 @@ public class StochModel implements Model
 				log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes (");
 				log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), ");
 				log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n");
+				if (extra) log.print("State rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n");
 			}
 			if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) {
 				log.print("Transition rewards ("+i+"): ");
 				log.print(JDD.GetNumNodes(transRewards[i]) + " nodes (");
 				log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), ");
 				log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n");
+				if (extra) log.print("Transition rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n");
 			}
 		}
 	}