diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index ef830dc0be1706450b24907180e3bf4a99c07f9a..1561520d50b6c41c098dc8f853bce63d9fbe597e 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -11,7 +11,7 @@ import purescala.TypeTrees._
 import purescala.Definitions._
 import LinearEquations.elimVariable
 
-class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 300) {
+class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 600) {
   def attemptToApplyOn(problem: Problem): RuleResult = if(!problem.xs.exists(_.getType == Int32Type)) RuleInapplicable else {
 
     val TopLevelAnds(exprs) = problem.phi
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index bee26bf88a64e7f55684242b804200dba831d37a..5faa2859456ebf95a2ae9b80db6c1f9c91c94312 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -12,7 +12,7 @@ import purescala.Definitions._
 import LinearEquations.elimVariable
 import leon.synthesis.Algebra.lcm
 
-class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 300) {
+class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 600) {
   def attemptToApplyOn(problem: Problem): RuleResult = {
     val TopLevelAnds(exprs) = problem.phi
 
@@ -31,8 +31,16 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
     val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
     val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
     val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains(_))
+
     if(candidateVars.isEmpty) RuleInapplicable else {
-      val processedVar = candidateVars.head
+      val processedVar: Identifier = candidateVars.map(v => {
+        val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(v)).toList)
+        if(normalizedLhs.isEmpty)
+          (v, 0)
+        else
+          (v, lcm(normalizedLhs.map{ case List(t, IntLiteral(i)) => if(i == 0) 1 else i.abs case _ => sys.error("shouldn't happen") }))
+      }).toList.sortWith((t1, t2) => t1._2 <= t2._2).head._1
+
       val otherVars: List[Identifier] = problem.xs.filterNot(_ == processedVar)
 
       val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(processedVar)).toList)