From 69dbb1a2200842e09276b4ad42d7c337817deb98 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 18 Apr 2013 15:57:34 +0200
Subject: [PATCH] if no counter-example is found by the disprover, return a
reasoner failure instead of modifying the proof tree (to act more like pp
does)
---
.../disprover/core/internal/DisproverReasoner.java | 10 ++++------
1 file changed, 4 insertions(+), 6 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 f388a87c..d6c00235 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
@@ -117,10 +117,9 @@ public class DisproverReasoner implements IReasoner {
IAntecedent ante = ProverFactory.makeAntecedent(goal);
- if (counterExample.timeoutOccured()) {
+ if (counterExample.timeoutOccured())
return ProverFactory.reasonerFailure(this, input,
"Timeout occurred (ProB)");
- }
if (!counterExample.counterExampleFound() && counterExample.isProof())
return ProverFactory.makeProofRule(this, input, sequent.goal(),
@@ -128,14 +127,13 @@ public class DisproverReasoner implements IReasoner {
"ProB (all cases checked)");
if (!counterExample.counterExampleFound())
- return ProverFactory.makeProofRule(this, input, null, null,
- IConfidence.DISCHARGED_MAX,
- "No Counter-Example found (ProB)", ante);
+ return ProverFactory
+ .reasonerFailure(this, input,
+ "No Counter-Example found (ProB), but there might exist one");
return ProverFactory.makeProofRule(this, input, null, null,
IConfidence.PENDING,
"Counter-Example: " + counterExample.toString(), ante);
-
}
@Override
--
GitLab