From 8aae98fcad2f251c37f09f65c2c1ae8125fd2bcd Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Mon, 26 May 2014 11:23:27 +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
---
.../src/de/prob/eventb/disprover/core/DisproverReasoner.java | 5 +++++
1 file changed, 5 insertions(+)
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 8921c211..1c7f3f8c 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.");
--
GitLab