From ffac47aad897ac617b7e779eadee4b7d210d2378 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 19 Apr 2013 11:10:22 +0200
Subject: [PATCH] improve output of disprover
---
.../eventb/disprover/core/internal/DisproverReasoner.java | 6 +++---
1 file changed, 3 insertions(+), 3 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 d6c00235..33182f24 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
@@ -119,17 +119,17 @@ public class DisproverReasoner implements IReasoner {
if (counterExample.timeoutOccured())
return ProverFactory.reasonerFailure(this, input,
- "Timeout occurred (ProB)");
+ "ProB: Timeout occurred.");
if (!counterExample.counterExampleFound() && counterExample.isProof())
return ProverFactory.makeProofRule(this, input, sequent.goal(),
null, IConfidence.DISCHARGED_MAX,
- "ProB (all cases checked)");
+ "ProB (no enumeration / all cases checked)");
if (!counterExample.counterExampleFound())
return ProverFactory
.reasonerFailure(this, input,
- "No Counter-Example found (ProB), but there might exist one");
+ "ProB: No Counter-Example found, but there might exist one.");
return ProverFactory.makeProofRule(this, input, null, null,
IConfidence.PENDING,
--
GitLab