diff --git a/mytests/Termination2.scala b/mytests/Termination2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4ef5ba8b07ccbe508c4a88945f9ccf7faaf5231d
--- /dev/null
+++ b/mytests/Termination2.scala
@@ -0,0 +1,14 @@
+
+object Test {
+  def f(x: BigInt): BigInt = {
+    if (x == 0) {
+      0
+    } else if (x > 0) {
+      f(x-1)+2
+    } else if (x < 0) {
+      f(x+1)-2
+    } else {
+      33
+    }
+  } ensuring (_ == x*2)
+}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 32b35b18f28126014fb04a2e8e07399697c2a050..6afe9d72acffc34153179f77fc698e676da1030c 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -15,6 +15,16 @@ import scala.collection.mutable.{Map => MutableMap}
 trait StructuralSize {
 
   private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty
+  
+  private val absFun = new FunDef(
+      FreshIdentifier("abs", alwaysShowUniqueID = true),
+      Seq(), // no type params 
+      IntegerType, // returns BigInt
+      Seq(ValDef(FreshIdentifier("x", IntegerType, alwaysShowUniqueID = true))), 
+      DefType.MethodDef
+  )
+  
+  private val typedAbsFun = TypedFunDef(absFun, Seq(IntegerType))
 
   def size(expr: Expr) : Expr = {
     def funDef(ct: ClassType, cases: ClassType => Seq[MatchCase]): FunDef = {
@@ -66,6 +76,9 @@ trait StructuralSize {
       case TupleType(argTypes) => argTypes.zipWithIndex.map({
         case (_, index) => size(tupleSelect(expr, index + 1, true))
       }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
+      case IntegerType =>
+        println("here")
+        FunctionInvocation(typedAbsFun, Seq(expr)) 
       case _ => InfiniteIntegerLiteral(0)
     }
   }