diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java index 08d812015dd3d62d87e7cd89fa53b6922afec3d3..5e834b9c6832b3ff899e0c4a1edd2e60ae62d713 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java @@ -4,6 +4,9 @@ import java.util.HashSet; import java.util.Set; import org.eclipse.core.runtime.Status; +import org.eclipse.jface.dialogs.MessageDialog; +import org.eclipse.swt.widgets.Shell; +import org.eclipse.ui.PlatformUI; import org.eventb.core.IEventBProject; import org.eventb.core.IPOSequent; import org.eventb.core.ast.Predicate; @@ -183,6 +186,15 @@ public class DisproverReasoner implements IReasoner { System.out.println(sequent.toString() + ": Counter-Example for selected hypotheses found."); + Shell activeShell = PlatformUI.getWorkbench() + .getActiveWorkbenchWindow().getShell(); + MessageDialog + .openWarning( + activeShell, + "Goal not provable", + "ProB found a Counter-Example for the selected Hypotheses, Goal not provable from selected Hypotheses but may be provable with all Hypotheses.\n" + + counterExample.toString()); + return ProverFactory .reasonerFailure( this,