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 dac3f05e6632c561e37210688b758d13b5c3fbea..d8a105cccab1ed6e7956eb55fa3b9716ef904ce1 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 @@ -133,31 +133,43 @@ public class DisproverReasoner implements IReasoner { IAntecedent ante = ProverFactory.makeAntecedent(goal); - if (counterExample.timeoutOccured()) + if (counterExample.timeoutOccured()) { + System.out.println(sequent.toString() + ": Timeout occured."); return ProverFactory.reasonerFailure(this, input, "ProB: Timeout occurred."); + } - if (!counterExample.counterExampleFound() && counterExample.isProof()) + if (!counterExample.counterExampleFound() && counterExample.isProof()) { + System.out.println(sequent.toString() + ": Proof."); return ProverFactory.makeProofRule(this, input, sequent.goal(), null, IConfidence.DISCHARGED_MAX, "ProB (no enumeration / all cases checked)"); + } + + if (!counterExample.counterExampleFound()) { + System.out.println(sequent.toString() + ": Unsure."); - if (!counterExample.counterExampleFound()) return ProverFactory.reasonerFailure( this, input, "ProB: No Counter-Example found due to " + counterExample.getReason() + ", but there might exist one."); + } if (counterExample.counterExampleFound() - && counterExample.onlySelectedHypotheses()) + && counterExample.onlySelectedHypotheses()) { + System.out.println(sequent.toString() + + ": Counter-Example for selected hypotheses found."); + return ProverFactory .reasonerFailure( this, input, "ProB: Counter-Example for selected Hypotheses found, Goal not provable from selected Hypotheses (may be provable with all Hypotheses)"); + } + System.out.println(sequent.toString() + ": Counter-Example found."); return ProverFactory.makeProofRule(this, input, null, null, IConfidence.PENDING, counterExample.toString(), ante); }