diff --git a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
index 5b17b6305645278641a89f67ab5ca611c1a8ad53..31439404574680d43e4dc95d1db19147363e8a05 100644
--- a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java
@@ -18,7 +18,7 @@ import de.prob.prolog.term.PrologTerm;
 public class ConstraintBasedAssertionCheckCommand implements IComposableCommand {
 
 	public static enum ResultType {
-		INTERRUPTED, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE
+		INTERRUPTED, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE_FOUND, NO_COUNTER_EXAMPLE_EXISTS
 	};
 
 	private static final String COMMAND_NAME = "cbc_static_assertion_violation_checking";
@@ -59,7 +59,9 @@ public class ConstraintBasedAssertionCheckCommand implements IComposableCommand
 		if (resultTerm.hasFunctor("interrupted", 0)) {
 			result = ResultType.INTERRUPTED;
 		} else if (resultTerm.hasFunctor("no_counterexample_found", 0)) {
-			result = ResultType.NO_COUNTER_EXAMPLE;
+			result = ResultType.NO_COUNTER_EXAMPLE_FOUND;
+		}  else if (resultTerm.hasFunctor("no_counterexample_exists", 0)) {
+			result = ResultType.NO_COUNTER_EXAMPLE_EXISTS;
 		} else if (resultTerm.hasFunctor("counterexample_found", 2)) {
 			result = ResultType.COUNTER_EXAMPLE;
 			CompoundPrologTerm counterExampleTerm = (CompoundPrologTerm) resultTerm;
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
index 876a6b175ec9f51959b8bcff25d516833c44488a..4f8826d8280817a420e3f5c14c118903f7ee0498 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
@@ -47,7 +47,12 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
 			message = "ProB did not return a result";
 		} else {
 			switch (result) {
-			case NO_COUNTER_EXAMPLE:
+			case NO_COUNTER_EXAMPLE_EXISTS:
+				dialogType = MessageDialog.INFORMATION;
+				dialogTitle = "No Counter-Example Exists";
+				message = "No Counter-Example to the Context Theorems exists.";
+				break;
+			case NO_COUNTER_EXAMPLE_FOUND:
 				dialogType = MessageDialog.INFORMATION;
 				dialogTitle = "No Counter-Example Found";
 				message = "No Counter-Example to the Context Theorems was found.";