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 ca5c5cce8a5002a25827f3e4a30f6be6bb50e3eb..90e2286151dd2fc5d98a552666f504cc1ef372f3 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 @@ -30,6 +30,7 @@ import de.prob.core.PrologException; import de.prob.eventb.disprover.core.DisproverReasonerInput; import de.prob.exceptions.ProBException; import de.prob.logging.Logger; +import de.prob.unicode.UnicodeTranslator; public class DisproverReasoner implements IReasoner { @@ -73,13 +74,20 @@ public class DisproverReasoner implements IReasoner { Logger.info("Calling Disprover on Sequent"); Set<Predicate> hypotheses = new HashSet<Predicate>(); + StringBuilder hypothesesString = new StringBuilder(); for (Predicate predicate : sequent.hypIterable()) { hypotheses.add(predicate); - Logger.info("Disprover: Sending Hypothesis: " - + predicate.toString()); + hypothesesString.append(predicate.toString()); + hypothesesString.append(" & "); } + 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: " + goal.toString()); + Logger.info("Disprover: Sending Goal: " + + UnicodeTranslator.toAscii(goal.toString())); IEventBRoot root = getRoot(sequent);