- Discovered ugly bit in de-class code, which causes what seem to be

errors with --extravert: even if Alice is already occurring in the
  system, the name can be used.
- Added explicit level 2 encryption bound. This is technically
  incorrect, but for now it should work.

src/notes.txt

@@ -1,3 +1,7 @@
+- De-classification does not work as desired. The name Alice is used
+  even if it already occurs somehwere in the system, which is not what
+  we want.
+- Heuristic could also punish more initiators.
 - If no attack/state output is needed, maybe the attack heuristic should
   be simpler (which means just weighting the trace length etc.) in order
   to avoid uneccesary continuation of the search. Maybe even stop

src/prune_theorems.c

@@ -410,6 +410,15 @@ prune_theorems (const System sys)
 	    }
 	}
 
+      // To be on the safe side, we currently limit the encryption level to two. This is not a problem for known attacks, but should be addressed more carefully at some point.
+      /**
+       * @todo Fix untyped variables reasoning
+       */
+      if (term_encryption_level (b->term) > 2)
+	{
+	  return true;
+	}
+
       /**
        * Prune on the basis of hidelevel lemma
        */

src/system.c

@@ -1426,6 +1426,7 @@ selfSession (const System sys, const int run)
 	{
 	  // This agent was already in the seen list
 	  self_session = true;
+	  break;
 	}
       else
 	{
@@ -1466,7 +1467,7 @@ selfResponders (const System sys)
   run = 0;
   while (run < sys->maxruns)
     {
-      if (selfInitiator (sys, run))
+      if (selfResponder (sys, run))
 	{
 	  count++;
 	}