Fix explicit non-prob LTL checking with experiments

We did not perform a required deepCopy of the path expression before checking/replacing maximal state formulas, thus modifying the original expression, which breaks later model checking when doing experiments.

Found by Steffen Märcker.

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