diff --git a/src/modelchecker.c b/src/modelchecker.c
index 4fd465b..3543fd8 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -208,61 +208,77 @@ explorify (const System sys, const int run)
   flag = 0;
 
   /*
-   * Special check: if agents have been instantiated in such a way that no more claims need to be evaluated, then we can skip
-   * further traversal.
-   * Two cases: internal read or first read of a run; both are the first event of a run.
-   *
-   * Efficiency of the next check heavily relies on lazy L-R evaluation
+   * Special checks after (implicit) choose events; always first in run reads.
    */
   if (rd == sys->runs[run].start && rd->type == READ)
     {
+      int rid;
+
       if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
 	{
           /* this run is executed by an untrusted agent, do not explore */
           return 0;
 	}
-      else
-	{
-	  /* executed by trusted agent, but is there a claim left to explore? */
-	  if (sys->secrets == NULL)
-	    { /* there are no remaining secrecy claims to be checked */
-	      Roledef rdscan;
-	      int rid;
-	      int validclaim;
+      /* executed by trusted agent */
 
-	      rid = 0;
-	      validclaim = 0;
-	      /* check for each run */
-	      while (rid < sys->maxruns)
-		{ 
-		  /* are claims in this run evaluated anyway? */
-		  if (!untrustedAgent (sys, sys->runs[rid].agents))
-		    { /* possibly claims to be checked in this run */
-		      rdscan = runPointerGet(sys, rid);
-		      while (rdscan != NULL)
+      /* Special check 1: if agents have been instantiated in such a way that no more claims need to be evaluated, then we can skip
+       * further traversal.
+       */
+      if (sys->secrets == NULL)
+	{ /* there are no remaining secrecy claims to be checked */
+	  Roledef rdscan;
+	  int validclaim;
+
+	  rid = 0;
+	  validclaim = 0;
+	  /* check for each run */
+	  while (rid < sys->maxruns)
+	    { 
+	      /* are claims in this run evaluated anyway? */
+	      if (!untrustedAgent (sys, sys->runs[rid].agents))
+		{ /* possibly claims to be checked in this run */
+		  rdscan = runPointerGet(sys, rid);
+		  while (rdscan != NULL)
+		    {
+		      if (rdscan->type == CLAIM)
 			{
-			  if (rdscan->type == CLAIM)
-			    {
-		    	      /* force abort of loop */
-			      validclaim = 1;
-			      rdscan = NULL;
-			      rid = sys->maxruns;
-			    }
-			  else
-			    {
-			      rdscan = rdscan->next;
-			    }
+			  /* force abort of loop */
+			  validclaim = 1;
+			  rdscan = NULL;
+			  rid = sys->maxruns;
+			}
+		      else
+			{
+			  rdscan = rdscan->next;
 			}
 		    }
-		  rid++;
-		}
-	      if (validclaim == 0)
-		{ /* no valid claims, abort */
-		  return 0;
 		}
+	      rid++;
+	    }
+	  if (validclaim == 0)
+	    { /* no valid claims, abort */
+	      return 0;
 	    }
 	}
+      /* Special check 2: if all agents in each run send only encrypted stuff, and all agents are trusted,
+       * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not
+       * be violated anymore if they contain no terms that are encrypted with such keys */
+
+      //!@todo For now, there is no check that the runs only send publicly encrypted stuff! Just an assumption to be made true using static analysis.
+
+      /*
+      rid = 0;
+      while (rid < sys->maxruns)
+	{
+	  if (!untrustedAgent (sys, sys->runs[rid].agents))
+	    {
+	    }
+	  rid++;
+	}
+	*/
     }
+
+  /* Apparently, all is well, and we can explore further */
   if (executeStep (sys, run))
     {
       /* traverse the system after the step */