diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 55e83bf40692d3f6e9388e8ea0647eef31f58c2f..02475d69dc6fc85337f41613bfc8c9b69d723f7c 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -14,7 +14,10 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
     val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)
 
-    val candidates = p.as.filter(_.getType == IntegerType).combinations(2).toList.filter {
+    val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
+                    p.as.filter(_.getType == Int32Type).combinations(2)
+
+    val candidates = argsPairs.toList.filter {
       case List(a1, a2) =>
         val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2)))