diff --git a/src/main/java/avatartranslator/AvatarArithmeticOp.java b/src/main/java/avatartranslator/AvatarArithmeticOp.java
index 051e56af1215f364582c94a3dcd9fd15d64937f7..19f10503e8244aed90e6bc034d8713996b663008 100644
--- a/src/main/java/avatartranslator/AvatarArithmeticOp.java
+++ b/src/main/java/avatartranslator/AvatarArithmeticOp.java
@@ -53,7 +53,7 @@ public class AvatarArithmeticOp extends AvatarTerm {
     AvatarTerm term2;
     String operator;
 
-    private static final String [] knownOp = {"+", "-", "*"};
+    private static final String [] knownOp = {"+", "-", "*", "/"};
 
     public AvatarArithmeticOp (AvatarTerm _term1, AvatarTerm _term2, String _operator, Object _referenceObject) {
         super (_term1.getName () + _operator + _term2.getName (), _referenceObject);
diff --git a/src/main/java/avatartranslator/AvatarStateMachineElement.java b/src/main/java/avatartranslator/AvatarStateMachineElement.java
index 64384093f177d28b4265ae6563a948d14aea587f..7cd31738a32ac428c4c64ba1eacf90cf8da3fc1e 100644
--- a/src/main/java/avatartranslator/AvatarStateMachineElement.java
+++ b/src/main/java/avatartranslator/AvatarStateMachineElement.java
@@ -196,7 +196,7 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
 
         return false;
     }
-    
+
 
     public boolean inAnUpperStateOf(AvatarState _state) {
         if (_state == null) {
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index 01d12b6d73f36d424c17b64a34443e799c46d246..57953a87f05dc5a933fce9286ed04caf537fc6e0 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -231,10 +231,14 @@ public class AVATAR2ProVerif implements AvatarTranslator {
     protected static String translateTerm (AvatarTerm term, Map<AvatarAttribute, Integer> attributeCmp) {
         if (term instanceof AvatarAttribute) {
             AvatarAttribute attr = (AvatarAttribute) term;
+
             if (attributeCmp != null) {
+                TraceManager.addDev("Mae Attr name 1");
                 return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName (), attributeCmp.get (attr).toString ());
-            } else
-                return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName ());
+            } else {
+                TraceManager.addDev("Mae Attr name 2");
+                return AVATAR2ProVerif.makeAttrName(attr.getBlock().getName(), attr.getName());
+            }
         }
 
         if (term instanceof AvatarConstant) {
@@ -259,16 +263,18 @@ public class AVATAR2ProVerif implements AvatarTranslator {
 
                     return sb.toString ();
                 } else {
+                    TraceManager.addDev("ERROR=ZERO");
                     // TODO: raise error
                     return ZERO;
                 }
-            } catch (NumberFormatException e) { }
+            } catch (NumberFormatException e) {  TraceManager.addDev("ERROR=NFE");}
 
             return constant.getName ();
         }
 
         if (term instanceof AvatarArithmeticOp) {
             AvatarArithmeticOp op = (AvatarArithmeticOp) term;
+            TraceManager.addDev("TERM=" + op.toString());
             if (op.getOperator ().compareTo ("+") == 0) {
                 AvatarTerm t1, t2;
                 t1 = op.getTerm1 ();
@@ -279,6 +285,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
                     t2 = t;
                 } else if (!(t2 instanceof AvatarConstant)) {
                     // TODO: raise error
+                    TraceManager.addDev("ERROR= t2!=constant");
                     return null;
                 }
 
@@ -299,16 +306,19 @@ public class AVATAR2ProVerif implements AvatarTranslator {
                         return sb.toString ();
                     } else {
                         // TODO: raise error
+                        TraceManager.addDev("ERROR= max int");
                         return AVATAR2ProVerif.translateTerm(t1, attributeCmp);
                     }
                 } catch (NumberFormatException e) { 
                     // TODO: raise error
+                    TraceManager.addDev("ERROR= NumberFormatException");
                     return AVATAR2ProVerif.translateTerm(t1, attributeCmp);
                 }
 
 
             } else {
                 // TODO: raise error
+                TraceManager.addDev("ERROR= not a +");
                 return null;
             }
         }