Skip to content
Snippets Groups Projects
Commit 66917bbd authored by Sebastian Krings's avatar Sebastian Krings
Browse files

fix index out of bounds if the disprover is called on a sequent without hypotheses

parent 72aaba51
No related branches found
No related tags found
No related merge requests found
...@@ -77,11 +77,15 @@ public class DisproverReasoner implements IReasoner { ...@@ -77,11 +77,15 @@ public class DisproverReasoner implements IReasoner {
hypothesesString.append(predicate.toStringFullyParenthesized()); hypothesesString.append(predicate.toStringFullyParenthesized());
hypothesesString.append(" & "); hypothesesString.append(" & ");
} }
if (hypothesesString.length() == 0) {
Logger.info("Disprover: No Hypotheses");
} else {
hypothesesString.delete(hypothesesString.length() - 2, hypothesesString.delete(hypothesesString.length() - 2,
hypothesesString.length()); hypothesesString.length());
Logger.info("Disprover: Sending Hypotheses: " Logger.info("Disprover: Sending Hypotheses: "
+ UnicodeTranslator.toAscii(hypothesesString.toString())); + UnicodeTranslator.toAscii(hypothesesString.toString()));
}
Predicate goal = sequent.goal(); Predicate goal = sequent.goal();
Logger.info("Disprover: Sending Goal: " Logger.info("Disprover: Sending Goal: "
+ UnicodeTranslator.toAscii(goal.toStringFullyParenthesized())); + UnicodeTranslator.toAscii(goal.toStringFullyParenthesized()));
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment