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 6d69da66f19355ecb5b4ded4dd9532b5556ca8e4..9fc71c8ba39e75163a584008b580c30efdc1595b 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 @@ -77,11 +77,15 @@ public class DisproverReasoner implements IReasoner { hypothesesString.append(predicate.toStringFullyParenthesized()); hypothesesString.append(" & "); } - hypothesesString.delete(hypothesesString.length() - 2, - hypothesesString.length()); - Logger.info("Disprover: Sending Hypotheses: " - + UnicodeTranslator.toAscii(hypothesesString.toString())); + if (hypothesesString.length() == 0) { + Logger.info("Disprover: No Hypotheses"); + } else { + hypothesesString.delete(hypothesesString.length() - 2, + hypothesesString.length()); + Logger.info("Disprover: Sending Hypotheses: " + + UnicodeTranslator.toAscii(hypothesesString.toString())); + } Predicate goal = sequent.goal(); Logger.info("Disprover: Sending Goal: " + UnicodeTranslator.toAscii(goal.toStringFullyParenthesized()));