From 4eeb0eac5eae528eed60af9c5b44398ef69255fc Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Thu, 18 Apr 2013 10:03:52 +0200 Subject: [PATCH] return a reasoner failure instead of modifying the proof tree if a timeout occurs --- .../eventb/disprover/core/internal/DisproverReasoner.java | 7 ++----- 1 file changed, 2 insertions(+), 5 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 96d86607..a994c521 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 @@ -115,11 +115,8 @@ public class DisproverReasoner implements IReasoner { IAntecedent ante = ProverFactory.makeAntecedent(goal); if (counterExample.timeoutOccured()) { - return ProverFactory - .makeProofRule(this, input, null, null, - IConfidence.DISCHARGED_MAX, - "Timeout occurred (ProB)", ante); - + return ProverFactory.reasonerFailure(this, input, + "Timeout occurred (ProB)"); } if (!counterExample.counterExampleFound() && counterExample.isProof()) -- GitLab