diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java index d8a105cccab1ed6e7956eb55fa3b9716ef904ce1..2f935d439d8ff67c1e013cbfb2b868cd67df9abc 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverReasoner.java @@ -133,6 +133,11 @@ public class DisproverReasoner implements IReasoner { 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."); return ProverFactory.reasonerFailure(this, input,