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 8921c211d07660d93f00908d14b25c73a7fe7328..1c7f3f8c8ecf5220c35770faf0e2d09d5a775647 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 @@ -133,6 +133,11 @@ public class DisproverReasoner implements IReasoner { Predicate goal = sequent.goal(); IAntecedent ante = ProverFactory.makeAntecedent(goal); + + if (counterExample == null) { + return ProverFactory.reasonerFailure(this, input, + "ProB: Error occurred."); + } if (counterExample.timeoutOccured()) { System.out.println(sequent.toString() + ": Timeout occured.");