diff --git a/src/de/stups/probkodkod/KodkodAnalysis.java b/src/de/stups/probkodkod/KodkodAnalysis.java
index 3b01b5687270cacf336e3637ae1771630c202c9e..8e11a9f160f5858fcb3c1ff403fce43d8e1e0ddd 100644
--- a/src/de/stups/probkodkod/KodkodAnalysis.java
+++ b/src/de/stups/probkodkod/KodkodAnalysis.java
@@ -48,6 +48,7 @@ import de.stups.probkodkod.parser.node.AConstInnerexpression;
 import de.stups.probkodkod.parser.node.AConstInnerformula;
 import de.stups.probkodkod.parser.node.AConstInnerintexpression;
 import de.stups.probkodkod.parser.node.ADiffExprBinop;
+import de.stups.probkodkod.parser.node.ADivIntexprBinop;
 import de.stups.probkodkod.parser.node.AEmptyExprConst;
 import de.stups.probkodkod.parser.node.AEqualsIntCompOp;
 import de.stups.probkodkod.parser.node.AEqualsLogopRel;
@@ -195,6 +196,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
 		BININTEXPROPS.put(ASubIntexprBinop.class.getName(), IntOperator.MINUS);
 		BININTEXPROPS.put(AMulIntexprBinop.class.getName(),
 				IntOperator.MULTIPLY);
+		BININTEXPROPS.put(ADivIntexprBinop.class.getName(), IntOperator.DIVIDE);
 
 		BININTCOMPS.put(AEqualsIntCompOp.class.getName(), IntCompOperator.EQ);
 		BININTCOMPS.put(AGreaterIntCompOp.class.getName(), IntCompOperator.GT);
diff --git a/src/problem.grammar b/src/problem.grammar
index ff4ed488be658662883b0f66e6ae5cfc85f21aab..20a42d6a6c94fc17ccea9f2074a48824c247e02d 100644
--- a/src/problem.grammar
+++ b/src/problem.grammar
@@ -67,6 +67,7 @@ Tokens
   keyword_addition = 'add';
   keyword_subtraction = 'sub';
   keyword_multiplication = 'mul';
+  keyword_division = 'div';
   keyword_greater = 'gt';
   keyword_greater_equal = 'gte';
   keyword_lesser = 'lt';
@@ -199,7 +200,8 @@ Productions
   intexpr_binop =
       {add}       keyword_addition
     | {sub}       keyword_subtraction
-    | {mul}       keyword_multiplication;  
+    | {mul}       keyword_multiplication
+    | {div}       keyword_division;  
 
   request = keyword_request [problem]:identifier [size]:number reqtype [al]:parenl [arguments]:argument* [ar]:parenr;
   argument = parenl identifier [tuples]:tuple* parenr;