diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java
index 20e1197ab3fa999549dd19a371bbc1ec28e6bac4..5715f2acb509fb7b3089971093ede6171aec74fa 100644
--- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java
+++ b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java
@@ -123,7 +123,7 @@ public class OpenObserverAction extends SelectionAction {
 				}
 
 			} else {
-				Logger.notifyUserWithoutBugreport("The Observer \""
+				Logger.notifyUser("The Observer \""
 						+ observer.getName()
 						+ "\" does not support a wizard.");
 			}
diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java
index cf5b463c09ec1749919bad45bf2d1ea3a5bbd6aa..2a26f4136988ccf6084062d73d16ce1a618cf0ce 100644
--- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java
+++ b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java
@@ -124,7 +124,7 @@ public class OpenSchedulerEventAction extends SelectionAction {
 					}
 
 				} else {
-					Logger.notifyUserWithoutBugreport("The Scheduler Event \""
+					Logger.notifyUser("The Scheduler Event \""
 							+ newSchedulerEvent.getName()
 							+ "\" does not support a wizard.");
 				}
diff --git a/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java b/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java
index c38986a76313d9eecabb69e96e42b0b4af75c3e0..bbbe41b0e02e55245b74bae159a703dab9fec559 100644
--- a/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java
+++ b/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java
@@ -23,9 +23,8 @@ public abstract class ProBJobFinishedListener extends JobChangeAdapter {
 				showResult(checkJob.getCommand(), checkJob.getAnimator());
 			}
 		} else {
-			final String message = "The job has a wrong type. Expected ProBCommandJob but got "
-					+ job.getClass();
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("The job has a wrong type. Expected ProBCommandJob but got "
+					+ job.getClass());
 		}
 	}
 
diff --git a/de.prob.core/src/de/prob/core/PrologException.java b/de.prob.core/src/de/prob/core/PrologException.java
index c5ce207798b4811f32dd920a52a64f43b8d60aef..84ae7bdf94cb3c15fe5ed51cce8e9a4eb92f0451 100644
--- a/de.prob.core/src/de/prob/core/PrologException.java
+++ b/de.prob.core/src/de/prob/core/PrologException.java
@@ -26,7 +26,7 @@ public class PrologException extends ProBException {
 		if (!handled) {
 			handled = true;
 			if (onlyWarnings) {
-				Logger.log(IStatus.WARNING, Logger.NOBUGREPORT,
+				Logger.log(IStatus.WARNING, Logger.NOTIFY_USER,
 						this.getMessage(), this);
 			} else {
 				Logger.notifyUser(this.getMessage(), this);
diff --git a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
index 98f0b1e5a27112cbd10cc5a02acf5c297e31823c..b162632661a6467928afdfd23020e666a98d4621 100644
--- a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
@@ -87,12 +87,12 @@ public final class ExploreStateCommand implements IComposableCommand {
 		// only show error message on SETUP_CONSTANTS and
 		// PARTIALLY_SETUP_CONSTANTS
 		if (unsatPropertiesExist) {
-			Logger.notifyUserWithoutBugreport("ProB could not find valid constants wich satisfy the properties.\n"
+			Logger.notifyUser("ProB could not find valid constants wich satisfy the properties.\n"
 					+ unsatPropsCommand.getUnsatPropertiesDescription());
 
 		} else if (!initialised && enabledOperations.isEmpty()
 				&& !timeoutOccured) {
-			Logger.notifyUserWithoutBugreport("ProB could not find valid constants/variables. This might be caused by the animation settings (e.g., Integer range or deferred set size) or by an inconsistency in the axioms.");
+			Logger.notifyUser("ProB could not find valid constants/variables. This might be caused by the animation settings (e.g., Integer range or deferred set size) or by an inconsistency in the axioms.");
 		}
 
 		Set<String> timeouts = new HashSet<String>(
diff --git a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java
index 4e81cec31e0a2f345c8a5bfcb53a002cf0f3d1df..9298bc226b6e5ad06d10d54df6e7af9c23ff2925 100644
--- a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java
+++ b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java
@@ -104,7 +104,7 @@ public final class LoadEventBModelCommand {
 							+ " Typically this means, that your axioms are too complicated for automatic solving. "
 							+ "You might create an animation refinement using the context menu to help ProB finding a solution.";
 				}
-				Logger.notifyUserWithoutBugreport(message);
+				Logger.notifyUser(message);
 			}
 		} catch (CommandException ex) {
 			Logger.notifyUser("Event-B Model or Context could not be loaded due to an exception: " 
diff --git a/de.prob.core/src/de/prob/core/internal/ServerConnection.java b/de.prob.core/src/de/prob/core/internal/ServerConnection.java
index a593d273f35faff3ce93117d418c1c64cefe1951..049253f22979ffacaa53d7e957b094a281957bfc 100644
--- a/de.prob.core/src/de/prob/core/internal/ServerConnection.java
+++ b/de.prob.core/src/de/prob/core/internal/ServerConnection.java
@@ -165,8 +165,7 @@ public class ServerConnection implements IServerConnection {
 			shutdown = false;
 		} else {
 			// This should never happen
-			final String message = "Tried to start a server that is already running";
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("Tried to start a server that is already running");
 		}
 	}
 
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 7cf350f8108d9236c0cef6b0349c268096c1757a..55f274f746bd13bdd27d890cb08bd9d97a22af6f 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
@@ -114,8 +114,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
 
 	public AEventBModelParseUnit getModelAST() {
 		if (broken) {
-			final String message = "The machine contains Rodin Problems. ProB will continue, but you may observe unexpected behaviour";
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("The machine contains Rodin Problems. ProB will continue, but you may observe unexpected behaviour");
 			return model;
 		}
 		return model;
diff --git a/de.prob.core/src/de/prob/logging/Logger.java b/de.prob.core/src/de/prob/logging/Logger.java
index 678c5ddce1eba6f6d1eb83772c35177e8e8b3258..e8d1d95be870ba5f90a5368808e213238bfce0f0 100644
--- a/de.prob.core/src/de/prob/logging/Logger.java
+++ b/de.prob.core/src/de/prob/logging/Logger.java
@@ -27,8 +27,7 @@ public final class Logger {
 	public static final int DEBUG = 0;
 	public static final int INFO = 1;
 	public static final int WARNING = 2;
-	public static final int BUGREPORT = 4;
-	public static final int NOBUGREPORT = 8;
+	public static final int NOTIFY_USER = 4;
 
 	/**
 	 * Registers a new {@link ILogListener}. The listener's
@@ -59,22 +58,13 @@ public final class Logger {
 	 */
 	public static void notifyUser(final String message,
 			final Throwable throwable) {
-		log(IStatus.ERROR, BUGREPORT, message, throwable);
+		log(IStatus.ERROR, NOTIFY_USER, message, throwable);
 	}
 
 	public static void notifyUser(final String message) {
 		notifyUser(message, null);
 	}
 
-	public static void notifyUserWithoutBugreport(final String message,
-			final Throwable throwable) {
-		log(IStatus.ERROR, NOBUGREPORT, message, throwable);
-	}
-
-	public static void notifyUserWithoutBugreport(final String message) {
-		notifyUserWithoutBugreport(message, null);
-	}
-
 	/**
 	 * Check a property. The method notifies the user and throws an exception if
 	 * the assertion fails. <br>
@@ -151,8 +141,4 @@ public final class Logger {
 	private static void log(final IStatus status) {
 		Activator.getDefault().getLog().log(status);
 	}
-
-	public static void notifyUserAboutWarningWithoutBugreport(String string) {
-		log(IStatus.WARNING, NOBUGREPORT, string, null);
-	}
 }
diff --git a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
index 6a3b4744a75fa558a81e4f407442c2aa074d469c..d3b2c16f4aba64452cd443a20fb99adbbb051b44 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
@@ -47,9 +47,7 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
 			ModelCheckingJob ccJob = (ModelCheckingJob) job;
 			showResult(ccJob.getModelCheckingResult());
 		} else {
-			final String message = "The job has a wrong type. Expected ModelCheckingJob but got "
-					+ job.getClass();
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("The job has a wrong type. Expected ModelCheckingJob but got " + job.getClass());
 		}
 	}
 
diff --git a/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java b/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java
index c5832a0687232e40289c3e77577f165e4283a9a7..dc2f3e06c4b46ad77f24e014d05fb167c60c13fd 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java
@@ -36,7 +36,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler {
 
 		final String prob_location = getBinaryLocation();
 		if (prob_location == null) {
-			Logger.notifyUserWithoutBugreport("You need to specify a location for" + PROB_STANDALONE_NAME +". See Preferences -> ProB Standalone.");
+			Logger.notifyUser("You need to specify a location for" + PROB_STANDALONE_NAME +". See Preferences -> ProB Standalone.");
 		} else {
 			final IEventBRoot root = getSelection();
 			if (root != null) {
@@ -53,7 +53,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler {
 					runProBClassic(prob_location, tmp);
 				}
 			} else {
-			    Logger.notifyUserWithoutBugreport("You need to select a context or machine to open with " + PROB_STANDALONE_NAME);
+			    Logger.notifyUser("You need to select a context or machine to open with " + PROB_STANDALONE_NAME);
 			}
 		}
 		return null;
@@ -97,7 +97,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler {
 			new Thread(new ClassicConsole(output)).start();
 
 		} catch (IOException e) {
-			Logger.notifyUserWithoutBugreport("You need to specify a correct location for "
+			Logger.notifyUser("You need to specify a correct location for "
 			+ PROB_CLASSIC_NAME + ". See Preferences -> ProB Standalone.\n"
 			+ PROB_CLASSIC_NAME + " location: "+ probBinary + 
 			 "\nModel file: " + modelFile +
@@ -121,7 +121,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler {
 			new Thread(new ClassicConsole(voutput)).start();
 			vprocess.waitFor(); // this blocks Rodin
 	        if (vprocess.exitValue() != 0) {
-				Logger.notifyUserWithoutBugreport("Failed to start java -version. Exit code: " + vprocess.exitValue());
+				Logger.notifyUser("Failed to start java -version. Exit code: " + vprocess.exitValue());
 	        }
 			
 			final String[] command = {"java", "-jar", probBinary, "--machine-file", modelFile};
@@ -136,7 +136,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler {
 			
 		} catch (IOException | InterruptedException e) {
 //		} catch (IOException e) {
-			Logger.notifyUserWithoutBugreport("You need to specify a correct location for "
+			Logger.notifyUser("You need to specify a correct location for "
 			+ PROB2_NAME + ". See Preferences -> ProB Standalone.\n"
 			+ PROB2_NAME + " location: "+ probBinary + 
 			 "\nModel file: " + modelFile +
@@ -157,7 +157,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler {
 			temp = File.createTempFile("prob_", ".eventb");
 			temp.deleteOnExit();
 		} catch (IOException e) {
-			Logger.notifyUserWithoutBugreport("Something went wrong while saving temp file.\n"
+			Logger.notifyUser("Something went wrong while saving temp file.\n"
 					+ e.getLocalizedMessage());
 		}
 		return temp;
diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java
index 7ad28d5974a24fd3fbabc4499a96b1f97fbe733c..c041a905ab929ff6a99fd77b54510a070cecca1a 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java
@@ -17,6 +17,7 @@ import org.eclipse.core.resources.IResourceDelta;
 import org.eclipse.core.resources.ResourcesPlugin;
 import org.eclipse.core.runtime.CoreException;
 import org.eclipse.core.runtime.IPath;
+import org.eclipse.core.runtime.IStatus;
 import org.eclipse.jface.action.IAction;
 import org.eclipse.jface.viewers.ISelection;
 import org.eclipse.jface.viewers.IStructuredSelection;
@@ -92,10 +93,9 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler {
 			   Logger.info(stringBuffer.toString());
 			   LimitedLogger.getLogger().log(stringBuffer.toString(),rootElement.getElementName(), null);
 			} else if (realError)
-				Logger.notifyUserWithoutBugreport(stringBuffer.toString());
+				Logger.notifyUser(stringBuffer.toString());
 			else
-				Logger.notifyUserAboutWarningWithoutBugreport(stringBuffer
-						.toString());
+				Logger.log(IStatus.WARNING, Logger.NOTIFY_USER, stringBuffer.toString(), null);
 		} else {
 		     Animator.getAnimator().resetRodinProjectHasErrorsOrWarnings();
 		}
diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java
index c0c52be3bf8551c8a736b964f679c66295289773..2fc868c1599a8642dad1f9c994d2ea5026680c17 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java
@@ -68,8 +68,7 @@ public class StartDistributedModelcheckHandler extends AbstractHandler implement
 		final IFile resource = extractResource(rootElement);
 
 		if (!checkErrorMarkers(resource)) {
-			String message = "A model/context in your project contains Errors or Warnings. This can lead to unexpected behavior (e.g. missing variables) when animating.";
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("A model/context in your project contains Errors or Warnings. This can lead to unexpected behavior (e.g. missing variables) when animating.");
 		}
 		;
 
@@ -83,7 +82,7 @@ public class StartDistributedModelcheckHandler extends AbstractHandler implement
                     s = new Socket("localhost", 4444);
                     new ObjectOutputStream(s.getOutputStream()).writeObject(output);
                 } catch (IOException e) {
-                    Logger.notifyUserWithoutBugreport("unable to connect to master", e);
+                    Logger.notifyUser("unable to connect to master", e);
                 } finally {
                     if (s != null) {
                         try {
diff --git a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java
index 4bef5235041480ed300081c61d6b055ce1a6e62f..d3b1b1da953961dc0bc1e190147932c9fd00cbd9 100644
--- a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java
@@ -34,9 +34,7 @@ public class LtlCheckingFinishedListener extends JobChangeAdapter {
 				showResult(ltlJob.getModelCheckingResult());
 			}
 		} else {
-			final String message = "The job has a wrong type. Expected LtlCheckingJob but got "
-					+ job.getClass();
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("The job has a wrong type. Expected LtlCheckingJob but got " + job.getClass());
 		}
 	}
 
diff --git a/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java b/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java
index f11341d1073f334b83ecbed3f1472fe3fc6d91d0..8f739f954b4b2c8dbf0a148a932edb1251fa220a 100644
--- a/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java
+++ b/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java
@@ -27,7 +27,7 @@ public final class ProBLogListener implements ILogListener {
 
 		final int code = status.getCode();
 
-		if (code == Logger.BUGREPORT || code == Logger.NOBUGREPORT) {
+		if (code == Logger.NOTIFY_USER) {
 			display.asyncExec(new Runnable() {
 				public void run() {
 					String title = (status.getSeverity() == IStatus.ERROR) ? "An Error occured"