diff --git a/src/main/java/avatartranslator/AvatarBinaryGuard.java b/src/main/java/avatartranslator/AvatarBinaryGuard.java
index 070ef547e6d468ee21a29086df8692bc6c45fdd1..13771149cf1a15a1c0bc5b07d4cc5c3cea681d54 100644
--- a/src/main/java/avatartranslator/AvatarBinaryGuard.java
+++ b/src/main/java/avatartranslator/AvatarBinaryGuard.java
@@ -38,6 +38,8 @@
 
 package avatartranslator;
 
+import myutil.TraceManager;
+
 import java.util.Map;
 
 /**
@@ -74,6 +76,8 @@ public class AvatarBinaryGuard extends AvatarComposedGuard {
         return this.guardA.getAsString (translator) + translator.translateBinaryOp (this.binaryOp) + this.guardB.getAsString (translator);
     }
 
+
+
     @Override
     public AvatarBinaryGuard clone () {
         return new AvatarBinaryGuard (this.guardA.clone (), this.guardB.clone (), this.binaryOp);
diff --git a/src/main/java/avatartranslator/AvatarComposedGuard.java b/src/main/java/avatartranslator/AvatarComposedGuard.java
index af75da1a4e92788bb069d80ea0a9d066ec415608..b4e1a3c08fd20d57a7dc76dd4f4220635bdf2856 100644
--- a/src/main/java/avatartranslator/AvatarComposedGuard.java
+++ b/src/main/java/avatartranslator/AvatarComposedGuard.java
@@ -38,6 +38,8 @@
 
 package avatartranslator;
 
+import myutil.TraceManager;
+
 /**
    * Class AvatarComposedGuard
    * Creation: 16/09/2015
@@ -47,7 +49,8 @@ package avatartranslator;
 public abstract class AvatarComposedGuard extends AvatarGuard {
     
 	public AvatarComposedGuard getOpposite () {
-        //return new AvatarUnaryGuard ("not", "(", ")", this);
+
+        // Otherwise, general case:
         return new AvatarUnaryGuard ("", "(", ") == false", this);
     }
 
diff --git a/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java b/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java
index d6aa10cb0a4c0669e59db53270b843d7a6f2a4e4..e5ff575d7be8a83dc4e4e4abe0ef146f1e7e8327 100644
--- a/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java
+++ b/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java
@@ -98,4 +98,28 @@ public class AvatarSimpleGuardDuo extends AvatarSimpleGuard {
             this.termB.replaceAttributes (attributesMapping);
         }
     }
+
+    public AvatarComposedGuard getOpposite () {
+        //return new AvatarUnaryGuard ("not", "(", ")", this);
+
+        // If guard is a binary guard, we take its opposite
+
+        String op = "";
+        if (binaryOp == "==") {
+            op = "!=";
+        } else if (binaryOp == "!=") {
+            op = "==";
+        }
+
+        if (op == null) {
+            // Otherwise, general case:
+            return new AvatarUnaryGuard("", "(", ") == false", this);
+        }
+
+        AvatarSimpleGuardDuo g = this.clone();
+        g.binaryOp = op;
+
+        return g;
+
+    }
 }
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index b5f23c48988884a5253fc1aec070cbd7def060a2..c9fc22f0e4e01fd78ba1ac4fddea9414afdf2d92 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -352,16 +352,18 @@ public class AVATAR2ProVerif implements AvatarTranslator {
     // -> transformed into a = b, a <> b, g1 && g2, g1 || g2
     // Returns nulls otherwise
     private static String translateGuard (AvatarGuard _guard, Map<AvatarAttribute, Integer> attributeCmp) {
-        TraceManager.addDev(_guard.toString());
-        if (_guard == null || _guard instanceof AvatarGuardEmpty)
+        TraceManager.addDev("Handling Guard:" + _guard.toString());
+        if (_guard == null || _guard instanceof AvatarGuardEmpty) {
+            TraceManager.addDev("Null or empty guard");
             return null;
+        }
 
         if (_guard instanceof AvatarGuardElse)
             // TODO: warning
             return null;
 
         if (_guard instanceof AvatarSimpleGuardMono) {
-            //TraceManager.addDev("SimpleGuardMono:" + _guard);
+            TraceManager.addDev("SimpleGuardMono:" + _guard);
             String term = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardMono) _guard).getTerm (), attributeCmp);
             //TraceManager.addDev("guard/ term=" + term);
             if (term != null)
@@ -371,7 +373,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
         }
 
         if (_guard instanceof AvatarSimpleGuardDuo) {
-            //TraceManager.addDev("SimpleGuardDuo");
+            TraceManager.addDev("SimpleGuardDuo");
             String delim = null;
             String termA = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermA (), attributeCmp);
             String termB = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermB (), attributeCmp);
@@ -392,7 +394,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
         }
 
         if (_guard instanceof AvatarUnaryGuard) {
-            //TraceManager.addDev("UnaryGuard");
+            TraceManager.addDev("UnaryGuard");
             String unary = ((AvatarUnaryGuard) _guard).getUnaryOp ();
             AvatarGuard guard = ((AvatarUnaryGuard) _guard).getGuard ();
 
@@ -406,6 +408,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
 
             String guardProV = AVATAR2ProVerif.translateGuard (guard, attributeCmp);
 
+
+
             if (beforeProV != null && guardProV != null)
                 return beforeProV + guardProV + afterProV;
 
@@ -413,7 +417,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
         }
 
         if (_guard instanceof AvatarBinaryGuard) {
-            //TraceManager.addDev("BinaryGuard");
+            TraceManager.addDev("BinaryGuard");
             String delim = ((AvatarBinaryGuard) _guard).getBinaryOp ();
             AvatarGuard guardA = ((AvatarBinaryGuard) _guard).getGuardA ();
             AvatarGuard guardB = ((AvatarBinaryGuard) _guard).getGuardB ();
@@ -433,7 +437,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
         }
 
         if (_guard instanceof AvatarConstantGuard) {
-            //TraceManager.addDev("ConstantGuard");
+            TraceManager.addDev("ConstantGuard");
             AvatarConstantGuard constant = (AvatarConstantGuard) _guard;
             if (constant.getConstant () == AvatarConstant.TRUE)
                 return "TRUE";
@@ -441,6 +445,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
                 return "FALSE";
         }
 
+        TraceManager.addDev("No valid guard found");
         return null;
     }
 
@@ -1367,8 +1372,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
                 AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB ();
                 if (attrA.getAttribute ().getBlock () ==  arg.block && attrA.getState ().getName ().equals (_asme.getName ())) {
                     TraceManager.addDev ("DEBUG: " + attrA.getAttribute ());
-                    TraceManager.addDev ("DEBUG: " + attrA.getAttribute ().getBlock ());
-                    TraceManager.addDev ("DEBUG: " + arg.attributeCmp.get (attrA.getAttribute()));
+                    //TraceManager.addDev ("DEBUG: " + attrA.getAttribute ().getBlock ());
+                    //TraceManager.addDev ("DEBUG: " + arg.attributeCmp.get (attrA.getAttribute()));
                     String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), arg.attributeCmp.get (attrA.getAttribute ()).toString ()) + ")";
                     if (!authenticityEvents.contains (sp)) {
                         authenticityEvents.add (sp);