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 27c3e2e805fe6155ea2338f7778ee5af35976d21..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;
 
@@ -69,7 +70,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			throws TranslationFailedException {
 		ContextTranslator contextTranslator = new ContextTranslator(context);
 		try {
-			(new TheoryTranslator()).translate();
 			contextTranslator.translate();
 		} catch (RodinDBException e) {
 			final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
@@ -136,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();
@@ -161,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 5f015c247dc4809b9e830aae1c0c822fa1381f11..ed82d8a8e8ee13b70b2e191805fa67b5168c306b 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
@@ -104,7 +104,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;
 	}
 
 }