Treat exists as proved if true

nickbattle · Sep 10, 2023 · 98cdf7f · 98cdf7f
1 parent c4e4962
commit 98cdf7f
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
@@ -51,6 +51,7 @@
 import com.fujitsu.vdmj.runtime.ContextException;
 import com.fujitsu.vdmj.runtime.Interpreter;
 import com.fujitsu.vdmj.runtime.RootContext;
+import com.fujitsu.vdmj.tc.expressions.TCExistsExpression;
 import com.fujitsu.vdmj.tc.expressions.TCExpression;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
 import com.fujitsu.vdmj.util.GetResource;
@@ -442,7 +443,17 @@ else if (result instanceof BooleanValue)
 				{
 					if (result.boolValue(ctxt))
 					{
-						String outcome = (results.proved) ? "PROVED" : "PASSED";
+						String outcome = null;
+
+						if (po.getCheckedExpression() instanceof TCExistsExpression)
+						{
+							outcome = "PROVED";		// Any "true" of an exists is PROVED.
+						}
+						else
+						{
+							outcome = (results.proved) ? "PROVED" : "PASSED";
+						}
+
 						printf("PO #%d, %s %s\n", po.number, outcome, duration(before, after));
 					}
 					else