From 8c044b7b3799aa330bf376f2d800e25c4315fc63 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 15 Jan 2015 12:12:43 +0100
Subject: [PATCH] submit all hypotheses back to rodin as used hypotheses to
 prevent false replay of disprover proof rules

---
 .../eventb/disprover/core/DisproverReasoner.java    | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

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 08d81201..e7e51182 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
@@ -147,6 +147,13 @@ public class DisproverReasoner implements IReasoner {
 
 		Predicate goal = sequent.goal();
 
+		// currently, we assume that all existing hypotheses have been used
+		// TODO: make ProB figure out which ones were actually used
+		Set<Predicate> usedHyps = new HashSet<Predicate>();
+		for (Predicate predicate : sequent.hypIterable()) {
+			usedHyps.add(predicate);
+		}
+
 		IAntecedent ante = ProverFactory.makeAntecedent(goal);
 
 		if (counterExample == null) {
@@ -163,7 +170,7 @@ public class DisproverReasoner implements IReasoner {
 		if (!counterExample.counterExampleFound() && counterExample.isProof()) {
 			System.out.println(sequent.toString() + ": Proof.");
 			return ProverFactory.makeProofRule(this, input, sequent.goal(),
-					null, IConfidence.DISCHARGED_MAX,
+					usedHyps, IConfidence.DISCHARGED_MAX,
 					"ProB (no enumeration / all cases checked)");
 		}
 
@@ -191,8 +198,8 @@ public class DisproverReasoner implements IReasoner {
 		}
 
 		System.out.println(sequent.toString() + ": Counter-Example found.");
-		return ProverFactory.makeProofRule(this, input, null, null,
-				IConfidence.PENDING, counterExample.toString(), ante);
+		return ProverFactory.makeProofRule(this, input, sequent.goal(),
+				usedHyps, IConfidence.PENDING, counterExample.toString(), ante);
 	}
 
 	@Override
-- 
GitLab