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 11473462710ba683718770550113f60d4e89cff4..eb881e5f4e2ba7ba7926c6d6573faa0ee9a3c115 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 @@ -122,7 +122,7 @@ public class DisproverReasoner implements IReasoner { ICounterExample counterExample = DisproverCommand.disprove( Animator.getAuxAnimator(), evbProject, allHypotheses, selectedHypotheses, goal, timeoutFactor, context, pm); - // Logger.info("Disprover: Result: " + counterExample.toString()); + Logger.info("Disprover: Result: " + counterExample.toString()); return counterExample; } @@ -197,12 +197,12 @@ public class DisproverReasoner implements IReasoner { && counterExample.onlySelectedHypotheses()) { System.out.println(sequent.toString() + ": Counter-Example for selected hypotheses found."); - + Sysemt.out.println(counterExample.toString()); return ProverFactory .reasonerFailure( this, input, - "ProB: Counter-Example for selected Hypotheses found, Goal not provable from selected Hypotheses (may be provable with all Hypotheses)"); + "ProB: Counter-Example to Goal for selected Hypotheses found (may be provable with all Hypotheses): " + counterExample.toString()); // use abbreviate or substring(0, Math.min(s.length(), 100)); } System.out.println(sequent.toString() + ": Counter-Example found.");