diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index a7a47c8a6c5f40a841dbeedb7c861e5f1b49638d..0d465014979e7c11e5e2b980b7381bc057a0314a 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1414,10 +1414,28 @@ object TreeOps {
       val na = f(a)
       if(a == na) a else fix(f)(na)
     }
+      
+
     val res = fix(simplePostTransform(simplify0))(expr)
     res
   }
 
+  def expandAndSimplifyArithmetic(expr: Expr): Expr = {
+    println("got: " + expr)
+    val expr0 = try {
+      val freeVars: Array[Identifier] = variablesOf(expr).toArray
+      val coefs: Array[Expr] = TreeNormalizations.linearArithmeticForm(expr, freeVars)
+      coefs.toList.zip(IntLiteral(1) :: freeVars.toList.map(Variable(_))).foldLeft[Expr](IntLiteral(0))((acc, t) => {
+        if(t._1 == IntLiteral(0)) acc else Plus(acc, Times(t._1, t._2))
+      })
+    } catch {
+      case _ => expr
+    }
+    val res = simplifyArithmetic(expr0)
+    println("simplified to: " + res)
+    res
+  }
+
   //Simplify the expression, applying all the simplify for various theories
   //Maybe it would be a good design decision to not have any simplify calling
   //an underlying solver, to somehow keep it light and become a function we call often