diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index 425266e84a5ea82463e71d46b129c5bbdac0e078..ad5b33afb304accdbaa9f275db0e8a47d91b6707 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -53,6 +53,7 @@ import de.be4.classicalb.core.parser.node.PSet;
 import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.hhu.stups.sablecc.patch.SourcePosition;
 import de.prob.core.translator.TranslationFailedException;
+import de.prob.eventb.translator.internal.EProofStatus;
 import de.prob.eventb.translator.internal.ProofObligation;
 import de.prob.eventb.translator.internal.SequentSource;
 
@@ -135,8 +136,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			final int confidence = status.getConfidence();
 			boolean broken = status.isBroken();
 
-			boolean discharged = !broken
-					&& confidence == IConfidence.DISCHARGED_MAX;
+			EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+			if (!broken && confidence == IConfidence.REVIEWED_MAX)
+				pstatus = EProofStatus.REVIEWED;
+			if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+				pstatus = EProofStatus.PROVEN;
 
 			IPOSequent sequent = status.getPOSequent();
 			IPOSource[] sources = sequent.getSources();
@@ -160,7 +165,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 						.getLabel()));
 
 			}
-			proofs.add(new ProofObligation(origin, s, name, discharged));
+			proofs.add(new ProofObligation(origin, s, name, pstatus));
 		}
 
 	}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java b/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
new file mode 100644
index 0000000000000000000000000000000000000000..160bf968ce3bd637dea4af99e8b5eea6ee72fd8f
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EProofStatus.java
@@ -0,0 +1,15 @@
+package de.prob.eventb.translator.internal;
+
+public enum EProofStatus {
+	UNPROVEN("false"), PROVEN("true"), REVIEWED("reviewed");
+	private final String text;
+
+	private EProofStatus(String text) {
+		this.text = text;
+	}
+
+	@Override
+	public String toString() {
+		return text;
+	}
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
index c733ac66be081a602bdf356dfcf302db1319d811..723d413d96db5ae8983e7f8763bf8023d9d2bb23 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
@@ -105,7 +105,7 @@ public abstract class EventBTranslator implements ITranslator {
 			}
 			pout.closeList();
 
-			pout.printAtom(Boolean.toString(proof.discharged));
+			pout.printAtom(proof.discharged.toString());
 			pout.closeTerm();
 		}
 
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index 95973e0f6975372dab6b1daa4ea1dc34e318d555..ead67da6ba447b4f830418088f54eb34069a3bf7 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -177,8 +177,12 @@ public class ModelTranslator extends AbstractComponentTranslator {
 			final int confidence = status.getConfidence();
 			boolean broken = status.isBroken();
 
-			boolean discharged = !broken
-					&& confidence == IConfidence.DISCHARGED_MAX;
+			EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+			if (!broken && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
+				pstatus = EProofStatus.REVIEWED;
+			if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+				pstatus = EProofStatus.PROVEN;
 
 			IPOSequent sequent = status.getPOSequent();
 			IPOSource[] sources = sequent.getSources();
@@ -202,7 +206,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
 				s.add(new SequentSource(type, le.getLabel()));
 
 			}
-			proofs.add(new ProofObligation(origin, s, name, discharged));
+			proofs.add(new ProofObligation(origin, s, name, pstatus));
 		}
 
 		if (!bugs.isEmpty()) {
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java b/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
index 978df176986cf410cc11e7acef776ac0305626b1..39b10069a3de8357e334a8f218384ae907ea96ae 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ProofObligation.java
@@ -9,14 +9,14 @@ public class ProofObligation {
 	public final IEventBRoot origin;
 	public final ArrayList<SequentSource> sources;
 	public final String kind;
-	public final boolean discharged;
+	public final EProofStatus discharged;
 
 	public ProofObligation(IEventBRoot origin, ArrayList<SequentSource> s,
-			String name, boolean discharged) {
+			String name, EProofStatus pstatus) {
 		this.origin = origin;
 		this.sources = s;
 		this.kind = name;
-		this.discharged = discharged;
+		this.discharged = pstatus;
 	}
 
 }