diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java
index 7ee9d96d..6aa36f8d 100644
--- a/prism/src/explicit/NonProbModelChecker.java
+++ b/prism/src/explicit/NonProbModelChecker.java
@@ -466,7 +466,7 @@ public class NonProbModelChecker extends StateModelChecker
 
 		LTLModelChecker ltlMC = new LTLModelChecker(this);
 		Vector<BitSet> labelBS = new Vector<BitSet>();
-		expr = ltlMC.checkMaximalStateFormulas(this, model, expr, labelBS);
+		expr = ltlMC.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelBS);
 
 		// We are doing existential LTL checking:
 		//  - Construct an NBA for the LTL formula