diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 38acf7ce..77267dc0 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -255,27 +255,28 @@ public class PrismCL
 						error(e.getMessage());
 					}
 				}
-			}
-			
-			// export labels/states
-			if (exportlabels) {
-				try {
-					if (propertiesFile != null) {
-						definedPFConstants = undefinedConstants.getPFConstantValues();
-						propertiesFile.setUndefinedConstants(definedPFConstants);
+				
+				// export labels/states
+				if (exportlabels) {
+					try {
+						if (propertiesFile != null) {
+							definedPFConstants = undefinedConstants.getPFConstantValues();
+							propertiesFile.setUndefinedConstants(definedPFConstants);
+						}
+						File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
+						prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
+					}
+					// in case of error, report it and proceed
+					catch (FileNotFoundException e) {
+						mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output");
+					}
+					catch (PrismException e) {
+						mainLog.println("\nError: " + e.getMessage() + ".");
 					}
-					File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
-					prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
-				}
-				// in case of error, report it and proceed
-				catch (FileNotFoundException e) {
-					mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output");
-				}
-				catch (PrismException e) {
-					mainLog.println("\nError: " + e.getMessage() + ".");
 				}
 			}
 			
+			
 			// work through list of properties to be checked
 			for (j = 0; j < numPropertiesToCheck; j++) {
 				
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 25d78875..f385d875 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -768,10 +768,14 @@ public class StateModelChecker implements ModelChecker
 			return checkExpressionFuncNary(expr);
 		case ExpressionFunc.FLOOR:
 		case ExpressionFunc.CEIL:
+		case ExpressionFunc.BIT_INV:
 			return checkExpressionFuncUnary(expr);
 		case ExpressionFunc.POW:
 		case ExpressionFunc.MOD:
 		case ExpressionFunc.LOG:
+		case ExpressionFunc.BIT_AND:
+		case ExpressionFunc.BIT_OR:
+		case ExpressionFunc.BIT_XOR:
 			return checkExpressionFuncBinary(expr);
 		default:
 			throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
@@ -803,6 +807,9 @@ public class StateModelChecker implements ModelChecker
 			case ExpressionFunc.CEIL:
 				dd1 = JDD.MonadicApply(JDD.CEIL, dd1);
 				break;
+			case ExpressionFunc.BIT_INV:
+				dd1 = JDD.MonadicApply(JDD.BIT_INV, dd1);
+				break;
 			}
 			return new StateProbsMTBDD(dd1, model);
 		}
@@ -819,6 +826,10 @@ public class StateModelChecker implements ModelChecker
 				for (i = 0; i < n; i++)
 					dv1.setElement(i, Math.ceil(dv1.getElement(i)));
 				break;
+			case ExpressionFunc.BIT_INV:
+				for (i = 0; i < n; i++)
+					dv1.setElement(i, ~((int)dv1.getElement(i)));
+				break;
 			}
 			return new StateProbsDV(dv1, model);
 		}
@@ -844,7 +855,8 @@ public class StateModelChecker implements ModelChecker
 			throw e;
 		}
 		// If both operands are symbolic, result will be symbolic
-		if (res1 instanceof StateProbsMTBDD && res2 instanceof StateProbsMTBDD) {
+		if (res1 instanceof StateProbsMTBDD && res2 instanceof StateProbsMTBDD)
+		{
 			dd1 = ((StateProbsMTBDD) res1).getJDDNode();
 			dd2 = ((StateProbsMTBDD) res2).getJDDNode();
 			switch (op) {
@@ -857,6 +869,15 @@ public class StateModelChecker implements ModelChecker
 			case ExpressionFunc.LOG:
 				dd = JDD.Apply(JDD.LOGXY, dd1, dd2);
 				break;
+			case ExpressionFunc.BIT_AND:
+				dd = JDD.Apply(JDD.BIT_AND, dd1, dd2);
+				break;
+			case ExpressionFunc.BIT_OR:
+				dd = JDD.Apply(JDD.BIT_OR, dd1, dd2);
+				break;
+			case ExpressionFunc.BIT_XOR:
+				dd = JDD.Apply(JDD.BIT_XOR, dd1, dd2);
+				break;					
 			}
 			return new StateProbsMTBDD(dd, model);
 		}
@@ -881,6 +902,18 @@ public class StateModelChecker implements ModelChecker
 				for (i = 0; i < n; i++)
 					dv1.setElement(i, PrismUtils.log(dv1.getElement(i), dv2.getElement(i)));
 				break;
+			case ExpressionFunc.BIT_AND:
+				for (i = 0; i < n; i++)
+					dv1.setElement(i, ((int)dv1.getElement(i)) & ((int)dv2.getElement(i)));
+				break;
+			case ExpressionFunc.BIT_OR:
+				for (i = 0; i < n; i++)
+					dv1.setElement(i, ((int)dv1.getElement(i)) | ((int)dv2.getElement(i)));
+				break;
+			case ExpressionFunc.BIT_XOR:
+				for (i = 0; i < n; i++)
+					dv1.setElement(i, ((int)dv1.getElement(i)) ^ ((int)dv2.getElement(i)));
+				break;
 			}
 			dv2.clear();
 			return new StateProbsDV(dv1, model);