diff --git a/src/avatartranslator/AvatarGuard.java b/src/avatartranslator/AvatarGuard.java
index 46043f147d6e3fa7490e51b01ebc997e967a0c36..1ac4db5233c9492be7313f570aa002ad3f3ff5b7 100644
--- a/src/avatartranslator/AvatarGuard.java
+++ b/src/avatartranslator/AvatarGuard.java
@@ -82,7 +82,7 @@ public abstract class AvatarGuard {
             indexRParen = AvatarGuard.getMatchingRParen (sane, 3);
             first = AvatarGuard.createFromString (block, sane.substring (4, indexRParen));
 
-            if (indexRParen == sane.length ()) {
+            if (indexRParen >= sane.length ()-1) {
                 if (first instanceof AvatarComposedGuard)
                     return new AvatarUnaryGuard ("not(", ")", (AvatarComposedGuard) first);
                 else
diff --git a/src/avatartranslator/AvatarGuardElse.java b/src/avatartranslator/AvatarGuardElse.java
index b2027a78dc9720c764be28eae919dc8d1fc46cd8..578f65fd32700788db9c27bfcefa8b0804bc986f 100644
--- a/src/avatartranslator/AvatarGuardElse.java
+++ b/src/avatartranslator/AvatarGuardElse.java
@@ -58,9 +58,11 @@ public class AvatarGuardElse extends AvatarGuard {
 
     public AvatarGuard getRealGuard (AvatarStateMachineElement precedent) {
         AvatarGuard result = null;
+
         for (AvatarStateMachineElement asme: precedent.getNexts ()) {
             if (! (asme instanceof AvatarTransition))
                 continue;
+
             AvatarGuard guard = ((AvatarTransition) asme).getGuard ();
             if (guard == this)
                 continue;
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index a86f6da47d83df212b08bda184d5c212c6ab1abd..6a246b014ec62966a822f3f819e22c4e8cd6996e 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -269,13 +269,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
             if (pragma instanceof AvatarPragmaSecrecyAssumption)
                 for (AvatarAttribute attribute: pragma.getArgs ()) {
                     AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
-                    if (trueAttr == null) {
-                        CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "You can't test confidentiality of attribute " + attribute.getBlock ().getName () + "." + attribute.getName () + " unless you declare it as initial knowledge.");
-                        ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarBDPanel());
-                        ce.setTGComponent((TGComponent)pragma.getReferenceObject ());
-                        warnings.add(ce);
-                        continue;
-                    }
+                    if (trueAttr == null)
+                        trueAttr = attribute;
                     if (secrecyChecked.contains (trueAttr))
                         continue;
 
@@ -293,13 +288,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
             if (pragma instanceof AvatarPragmaSecret)
                 for (AvatarAttribute attribute: pragma.getArgs ()) {
                     AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
-                    if (trueAttr == null) {
-                        CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "You can't test confidentiality of attribute " + attribute.getBlock ().getName () + "." + attribute.getName () + " unless you declare it as initial knowledge.");
-                        ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarBDPanel());
-                        ce.setTGComponent((TGComponent)pragma.getReferenceObject ());
-                        warnings.add(ce);
-                        continue;
-                    }
+                    if (trueAttr == null)
+                        trueAttr = attribute;
                     if (secrecyChecked.contains (trueAttr))
                         continue;
 
@@ -949,6 +939,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
 
         if (nbOfNexts == 1) {
             arg.lastInstr = _lastInstr;
+            arg.lastASME = _asme;
             this.translateNext (_asme.getNext(0), arg);
 
         } else if (_asme.hasElseChoiceType1()) {
@@ -958,10 +949,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
             HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> (arg.attributeCmp);
 
             arg.lastInstr = _lastInstr.setNextInstr (ite);
+            arg.lastASME = _asme;
             this.translateNext (_asme.getNext (0).getNext (0), arg);
 
             arg.attributeCmp = attributeCmp;
             arg.lastInstr = ite.getElse ();
+            arg.lastASME = _asme;
             this.translateNext (_asme.getNext (1).getNext (0), arg);
 
         } else {
@@ -988,6 +981,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
 
             arg.attributeCmp = attributeCmp;
             arg.lastInstr = _lastInstr;
+            arg.lastASME = _asme;
             this.translateNext (_asme.getNext (nbOfNexts-1), arg);
         }
     }
@@ -1014,6 +1008,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
         }
 
         arg.lastInstr = _lastInstr;
+        arg.lastASME = _asme;
         this.translateNext (_asme.getNext(0), _arg);
     }
 
diff --git a/src/proverifspec/ProVerifSyntaxer.java b/src/proverifspec/ProVerifSyntaxer.java
index cc6ad316570b6e738b62bb4f82385c2549cf9614..9ed8d2440c939f8edbadabb7e8b456ee88d5c31e 100644
--- a/src/proverifspec/ProVerifSyntaxer.java
+++ b/src/proverifspec/ProVerifSyntaxer.java
@@ -124,8 +124,13 @@ public abstract class ProVerifSyntaxer {
     protected void translateProcITE (ProVerifProcITE _node, int _alinea) {
         this.fullSpec += "\n" + this.printAlinea (_alinea);
         this.fullSpec += "if " + _node.cond + " then";
-        if (_node.next != null)
+        if (_node.next != null) {
+            if (_node.elseInstr.next != null)
+                this.fullSpec += " (";
             this.translate (_node.next, _alinea+1);
+            if (_node.elseInstr.next != null)
+                this.fullSpec += ")";
+        }
         else
             this.fullSpec += " 0";
         if (_node.elseInstr.next != null) {
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index c8dd4c980faa7e068c7ad8f2137a9c8db33ffc01..abc9009b41d65a279471dd1bee7a45fed7a185ae 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -341,7 +341,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
 
         // Confidential attributes
         for(AvatarAttribute attribute: pvoa.getSecretTerms()) {
-            TAttribute a = abdp.getAttributeByBlockName(attribute.getBlock ().getName (), attribute.getName ());
+            TAttribute a = abdp.getAttributeByBlockName(attribute.getBlock ().getName (), attribute.getName ().split ("_")[0]);
             if (a != null)
                 //TraceManager.addDev("Setting conf to ok");
                 a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);