diff --git a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java
index b49836e07..fdbe2f9df 100644
--- a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java
+++ b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java
@@ -120,7 +120,7 @@ else if (def instanceof POImplicitOperationDefinition)
 			{
 				JSONArray constructors = null;
 				
-				results.add(makeLens(po.location, "Counterexample", CODE_LENS_COMMAND,
+				results.add(makeLens(po.location, "PO #" + po.number, CODE_LENS_COMMAND,
 						launchArgs(launchName, defaultName, true, constructors, applyName, applyTypes, applyArgs)));
 			}
 		}
diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java
index b02bc88e5..84616e9d0 100644
--- a/lsp/src/main/java/workspace/plugins/POPlugin.java
+++ b/lsp/src/main/java/workspace/plugins/POPlugin.java
@@ -143,7 +143,8 @@ else if (event instanceof CodeLensEvent)
 
 	protected void preCheck(CheckPrepareEvent event)
 	{
-		// Nothing
+		messagehub.clearPluginMessages(this);
+		clearLenses();
 	}
 
 	/**
@@ -268,7 +269,7 @@ private JSONArray getCodeLenses(File file)
 		{
 			for (POLaunchDebugLens lens: codeLenses.get(file))
 			{
-				results.add(lens.getLaunchLens());
+				results.addAll(lens.getLaunchLens());
 			}
 		}
 		
diff --git a/lsp/src/main/java/workspace/plugins/POPluginPR.java b/lsp/src/main/java/workspace/plugins/POPluginPR.java
index e35ce749f..b09961cfa 100644
--- a/lsp/src/main/java/workspace/plugins/POPluginPR.java
+++ b/lsp/src/main/java/workspace/plugins/POPluginPR.java
@@ -51,7 +51,6 @@ protected void preCheck(CheckPrepareEvent ev)
 		super.preCheck(ev);
 		poClassList = null;
 		obligationList = null;
-		messagehub.clearPluginMessages(this);
 	}
 
 	@SuppressWarnings("unchecked")
diff --git a/lsp/src/main/java/workspace/plugins/POPluginSL.java b/lsp/src/main/java/workspace/plugins/POPluginSL.java
index 21529007b..c39d12fe3 100644
--- a/lsp/src/main/java/workspace/plugins/POPluginSL.java
+++ b/lsp/src/main/java/workspace/plugins/POPluginSL.java
@@ -51,7 +51,6 @@ public void preCheck(CheckPrepareEvent ev)
 		super.preCheck(ev);
 		poModuleList = null;
 		obligationList = null;
-		messagehub.clearPluginMessages(this);
 	}
 
 	@SuppressWarnings("unchecked")