From 66917bbde36249d30b8106c985782e49e29e10fe Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Fri, 7 Jun 2013 13:45:45 +0200 Subject: [PATCH] fix index out of bounds if the disprover is called on a sequent without hypotheses --- .../disprover/core/internal/DisproverReasoner.java | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) 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 6d69da66..9fc71c8b 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())); -- GitLab