diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 08f4c0f060aab8cbb8f7fc6515613ac8537e10ef..f2158675fd435cabc422db005b7341fb3fa5d5c4 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1393,7 +1393,6 @@ object TreeOps {
       case Times(IntLiteral(i), UMinus(e)) => Times(IntLiteral(-i), e)
       case Times(UMinus(e), IntLiteral(i)) => Times(e, IntLiteral(-i))
       case Times(IntLiteral(i1), Division(e, IntLiteral(i2))) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), e)
-      case Times(IntLiteral(i1), Plus(Division(e1, IntLiteral(i2)), e2)) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), Plus(e1, e2))
 
       case Division(IntLiteral(i1), IntLiteral(i2)) if i2 != 0 => IntLiteral(i1 / i2)
       case Division(e, IntLiteral(1)) => e
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 87ae844ec3827ea5838a2a44491a1553c2afff71..763550e4433f4cc389750ec1b7317c344fee287f 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -61,6 +61,9 @@ class TreeOpsTests extends FunSuite {
     checkSameExpr(e4, simplify(e4), Set(xId))
     val e5 = Plus(x, Minus(x, IntLiteral(2)))
     checkSameExpr(e5, simplify(e5), Set(xId))
+
+    val e6 = Times(IntLiteral(9), Plus(Division(x, IntLiteral(3)), Division(x, IntLiteral(6))))
+    checkSameExpr(e6, simplify(e6), Set(xId))
   }