diff --git a/src/arachne.c b/src/arachne.c
index 67d0ada..a4973d9 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -111,7 +111,7 @@ arachneInit (const System mysys)
   add_event (READ, NULL);
   add_event (READ, NULL);
   add_event (SEND, NULL);
-  I_RRS = add_role ("I_D: Encrypt");
+  I_RRS = add_role ("I_E: Encrypt");
 
   return;
 }
@@ -172,12 +172,12 @@ semiRunCreate (const Protocol p, const Role r)
 {
   int run;
 
-  run = sys->maxruns;
   if (p == INTRUDER)
     num_intruder_runs++;
   else
     num_regular_runs++;
   roleInstance (sys, p, r, NULL, NULL);
+  run = sys->maxruns-1;
   sys->runs[run].length = 0;
   return run;
 }
@@ -186,14 +186,17 @@ semiRunCreate (const Protocol p, const Role r)
 void
 semiRunDestroy ()
 {
-  Protocol p;
+  if (sys->maxruns > 0)
+    {
+      Protocol p;
 
-  p = sys->runs[sys->maxruns - 1].protocol;
-  roleInstanceDestroy (sys);
-  if (p == INTRUDER)
-    num_intruder_runs--;
-  else
-    num_regular_runs--;
+      p = sys->runs[sys->maxruns - 1].protocol;
+      roleInstanceDestroy (sys);
+      if (p == INTRUDER)
+	num_intruder_runs--;
+      else
+	num_regular_runs--;
+    }
 }
 
 //! After a role instance, or an extension of a run, we might need to add some goals
@@ -765,6 +768,7 @@ bind_goal_new_m0 (const Binding b)
 	  goal_unbind (b);
 	  indentDepth--;
 	  semiRunDestroy ();
+
 	  termlistSubstReset (subst);
 	  termlistDelete (subst);
 	}
@@ -792,9 +796,11 @@ bind_goal_new_encrypt (const Binding b)
 {
   Term term;
   int flag;
+  int can_be_encrypted;
 
   flag = 1;
-  term = b->term;
+  term = deVar(b->term);
+  can_be_encrypted = 0;
 
   if (!realTermLeaf (term))
     {
@@ -804,7 +810,7 @@ bind_goal_new_encrypt (const Binding b)
       Roledef rd;
       Term t1, t2;
 
-      if (realTermTuple (term))
+      if (!realTermEncrypt (term))
 	{
 	  // tuple construction
 	  error ("Goal that is a tuple should not occur!");
@@ -814,41 +820,47 @@ bind_goal_new_encrypt (const Binding b)
       t1 = term->left.op;
       t2 = term->right.key;
 
-      run = semiRunCreate (INTRUDER, I_RRS);
-      rd = sys->runs[run].start;
-      rd->message = termDuplicate (t1);
-      rd->next->message = termDuplicate (t2);
-      rd->next->next->message = termDuplicate (term);
-      index = 2;
-      proof_suppose_run (run, 0, index + 1);
-      if (sys->output == PROOF)
+      if (t2 != TERM_Hidden)
 	{
-	  indentPrint ();
-	  eprintf ("* Encrypting ");
-	  termPrint (term);
-	  eprintf (" using term ");
-	  termPrint (t1);
-	  eprintf (" and key ");
-	  termPrint (t2);
-	  eprintf ("\n");
+	  can_be_encrypted = 1;
+	  run = semiRunCreate (INTRUDER, I_RRS);
+	  rd = sys->runs[run].start;
+	  //rd->message = termDuplicateUV (t1);
+	  //rd->next->message = termDuplicateUV (t2);
+	  rd->next->next->message = termDuplicateUV (term);
+	  index = 2;
+	  proof_suppose_run (run, 0, index + 1);
+	  if (sys->output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("* Encrypting ");
+	      termPrint (term);
+	      eprintf (" using term ");
+	      termPrint (t1);
+	      eprintf (" and key ");
+	      termPrint (t2);
+	      eprintf ("\n");
+	    }
+	  newgoals = add_read_goals (run, 0, index + 1);
+	  
+	  indentDepth++;
+	  if (goal_bind (b, run, index))
+	    {
+	      proof_suppose_binding (b);
+	      flag = flag && iterate ();
+	    }
+	  else
+	    {
+	      proof_cannot_bind (b, run, index);
+	    }
+	  goal_unbind (b);
+	  indentDepth--;
+	  remove_read_goals (newgoals);
+	  semiRunDestroy ();
 	}
-      newgoals = add_read_goals (run, 0, index + 1);
-      indentDepth++;
-      if (goal_bind (b, run, index))
-	{
-	  proof_suppose_binding (b);
-	  flag = flag && iterate ();
-	}
-      else
-	{
-	  proof_cannot_bind (b, run, index);
-	}
-      goal_unbind (b);
-      indentDepth--;
-      remove_read_goals (newgoals);
-      semiRunDestroy ();
     }
-  else
+
+  if (!can_be_encrypted)
     {
       if (sys->output == PROOF)
 	{
@@ -1375,26 +1387,25 @@ arachne ()
 	  proof_suppose_run (run, 0, cl->ev + 1);
 	  add_read_goals (run, 0, cl->ev + 1);
 
-
 	  /**
 	   * Add specific goal info
 	   */
 	  add_claim_specifics (cl,
 			       roledef_shift (sys->runs[run].start, cl->ev));
-
 #ifdef DEBUG
 	  if (DEBUGL (5))
 	    {
 	      printSemiState ();
 	    }
 #endif
-
-	  /*
-	   * iterate
-	   */
+	  // Iterate
 	  iterate ();
 
 	  //! Destroy
+	  while (sys->bindings != NULL)
+	    {
+	      remove_read_goals (1);
+	    }
 	  while (sys->maxruns > 0)
 	    {
 	      semiRunDestroy ();
diff --git a/src/term.c b/src/term.c
index 15d0fc8..c47270e 100644
--- a/src/term.c
+++ b/src/term.c
@@ -433,7 +433,7 @@ termDuplicate (const Term term)
     return term;
 
   newterm = (Term) memAlloc (sizeof (struct term));
-  newterm->type = term->type;
+  memcpy (newterm, term, sizeof (struct term));
   if (realTermEncrypt (term))
     {
       newterm->left.op = termDuplicate (term->left.op);
@@ -464,13 +464,9 @@ termDuplicateDeep (const Term term)
     return NULL;
 
   newterm = (Term) memAlloc (sizeof (struct term));
-  if (realTermLeaf (term))
+  memcpy (newterm, term, sizeof (struct term));
+  if (!realTermLeaf (term))
     {
-      memcpy (newterm, term, sizeof (struct term));
-    }
-  else
-    {
-      newterm->type = term->type;
       if (realTermEncrypt (term))
 	{
 	  newterm->left.op = termDuplicateDeep (term->left.op);
@@ -496,14 +492,14 @@ termDuplicateUV (Term term)
 {
   Term newterm;
 
+  term = deVar (term);
   if (term == NULL)
     return NULL;
-  term = deVar (term);
   if (realTermLeaf (term))
     return term;
 
   newterm = (Term) memAlloc (sizeof (struct term));
-  newterm->type = term->type;
+  memcpy (newterm, term, sizeof (struct term));
   if (realTermEncrypt (term))
     {
       newterm->left.op = termDuplicateUV (term->left.op);
@@ -676,7 +672,7 @@ tupleCount (Term tt)
     }
   else
     {
-      deVar (tt);
+      tt = deVar (tt);
       if (!realTermTuple (tt))
 	{
 	  return 1;
@@ -702,7 +698,7 @@ tupleProject (Term tt, int n)
     {
       return NULL;
     }
-  deVar (tt);
+  tt = deVar (tt);
   if (!realTermTuple (tt))
     {
       if (n > 0)
@@ -956,32 +952,62 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
 
 	  if (noder != NULL)
 	    flag = flag && noder (term);
+
+	  return flag;
 	}
     }
   return 1;
 }
 
-//! Generic term iteration with deVar
+//! Generic term iteration
 int
-term_iterate_deVar (const Term term, int (*leaf) (), int (*nodel) (),
-		    int (*nodem) (), int (*noder) ())
+term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
+	      int (*nodem) (), int (*noder) ())
 {
-  int deVar_leaf (const Term term)
-  {
-    if (substVar (term))
-      {
-	return term_iterate_deVar (term->subst, deVar_leaf, nodel, nodem,
-				   noder);
-      }
-    else
-      {
-	if (leaf == NULL)
-	  return 1;
-	else
-	  return leaf (term);
-      }
-  }
-  return term_iterate (term, deVar_leaf, nodel, nodem, noder);
+  term = deVar (term);
+  if (term != NULL)
+    {
+      if (realTermLeaf (term))
+	{
+	  // Leaf
+	  if (leaf != NULL)
+	    {
+	      return leaf (term);
+	    }
+	}
+      else
+	{
+	  int flag;
+
+	  flag = 1;
+
+	  if (nodel != NULL)
+	    flag = flag && nodel (term);
+
+	  if (realTermTuple (term))
+	    flag = flag
+	      && (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder));
+	  else
+	    flag = flag
+	      && (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
+
+	  if (nodem != NULL)
+	    flag = flag && nodem (term);
+
+	  if (realTermTuple (term))
+	    flag = flag
+	      && (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder));
+	  else
+	    flag = flag
+	      && (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
+
+	  if (noder != NULL)
+	    flag = flag && noder (term);
+
+	  return flag;
+	}
+    }
+  return 1;
 }
 
 //! Iterate over the leaves in a term
@@ -1082,26 +1108,36 @@ term_constrain_level (const Term term)
   int structure;
   int flag;
 
-  int leaf (const Term t)
-  {
-    structure++;
-    if (realTermVariable (t))
-      vars++;
-    return 1;
-  }
-  int nodel (const Term t)
-  {
-    structure++;
-    if (realTermTuple (t))
-	structure++;
-    return 1;
-  }
+  void
+  tcl_iterate (Term t)
+    {
+      t = deVar (t);
+      structure++;
+      if (realTermLeaf (t))
+	{
+	  if (realTermVariable (t))
+	      vars++;
+	}
+      else
+	{
+	  if (realTermTuple (t))
+	    {
+	      tcl_iterate (t->left.op1);
+	      tcl_iterate (t->right.op2);
+	    }
+	  else
+	    {
+	      tcl_iterate (t->left.op);
+	      tcl_iterate (t->right.key);
+	    }
+	}
+    }
 
   if (term == NULL)
     error ("Cannot determine constrain level of empty term.");
 
   vars = 0;
   structure = 0;
-  flag = term_iterate_deVar (term, leaf, nodel, NULL, NULL);
+  tcl_iterate (term);
   return ((float) vars / (float) structure);
 }
diff --git a/src/term.h b/src/term.h
index 44cd29c..2effd7b 100644
--- a/src/term.h
+++ b/src/term.h
@@ -170,7 +170,7 @@ float termDistance (Term t1, Term t2);
 int termOrder (Term t1, Term t2);
 int term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
 		  int (*nodem) (), int (*noder) ());
-int term_iterate_deVar (const Term term, int (*leaf) (), int (*nodel) (),
+int term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
 			int (*nodem) (), int (*noder) ());
 int term_iterate_leaves (const Term t, int (*func) ());
 int term_iterate_open_leaves (const Term term, int (*func) ());