From 9291845924d6487589277cc0ebe3d3326339b82a Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Mon, 26 May 2014 11:22:17 +0200
Subject: [PATCH] if counter-example is set to NULL because of an exception on
the Prolog side, the DisproverReasoner no longer throws a
NullPointerException but fails with an appropriate error message
---
.../eventb/disprover/core/internal/DisproverReasoner.java | 5 +++++
1 file changed, 5 insertions(+)
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 d8a105cc..2f935d43 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,
--
GitLab