From d73fda6ec9ce4365eee29f6984c0fa3b8c66c307 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 16 Feb 2016 12:39:08 +0000
Subject: [PATCH] symbolic LTL: fix recursion call for AU

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11203 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NonProbModelChecker.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java
index 62521795..d54f403a 100644
--- a/prism/src/prism/NonProbModelChecker.java
+++ b/prism/src/prism/NonProbModelChecker.java
@@ -205,7 +205,7 @@ public class NonProbModelChecker extends StateModelChecker
 				Expression rhs = new ExpressionTemporal(ExpressionTemporal.P_G, null, notPhi2);
 				rhs = Expression.Not(new ExpressionExists(rhs));
 				Expression enf = Expression.And(lhs, rhs);
-				res = checkExpressionExists(enf);
+				res = checkExpression(enf);
 			}
 			// Eventually (AF)
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_F) {