Small fix to termination checker for int32 termination

src/main/scala/leon/termination/Processor.scala

@@ -27,15 +27,8 @@ trait Solvable extends Processor {
 
   val modules: Strengthener with StructuralSize
 
-  private val solver: SolverFactory[Solver] = {
-    val program     : Program     = checker.program
-    val context     : LeonContext = checker.context
-    val sizeModule  : ModuleDef   = ModuleDef(FreshIdentifier("$size"), modules.defs.toSeq, false)
-    val sizeUnit    : UnitDef     = UnitDef(FreshIdentifier("$size"),Seq(sizeModule)) 
-    val newProgram  : Program     = program.copy( units = sizeUnit :: program.units)
-
-    SolverFactory.getFromSettings(context, newProgram).withTimeout(1.seconds)
-  }
+  private val solver: SolverFactory[Solver] =
+    SolverFactory.getFromSettings(checker.context, checker.program).withTimeout(1.seconds)
 
   type Solution = (Option[Boolean], Map[Identifier, Expr])
 

src/main/scala/leon/termination/RelationComparator.scala

@@ -76,19 +76,22 @@ trait BVRelationComparator extends RelationComparator { self : StructuralSize =>
   def isApplicableFor(p: Problem): Boolean = {
     p.funDefs.forall(fd => fd.params.exists(valdef => valdef.getType == Int32Type))
   }
-  
+
   def bvSize(e: Expr): Expr = FunctionInvocation(typedAbsIntFun, Seq(e))
 
+  /* Note: We swap the arguments to the `lexicographicDecreasing` call
+   * since bvSize maps into negative ints! (avoids -Integer.MIN_VALUE overflow) */
+
   def sizeDecreasing(s10: Seq[Expr], s20: Seq[Expr]): Expr = {
     val s1 = s10.filter(_.getType == Int32Type)
     val s2 = s20.filter(_.getType == Int32Type)
-    lexicographicDecreasing(s1, s2, strict = true, sizeOfOneExpr = bvSize)
+    lexicographicDecreasing(s2, s1, strict = true, sizeOfOneExpr = bvSize)
   }
 
   def softDecreasing(s10: Seq[Expr], s20: Seq[Expr]): Expr = {
     val s1 = s10.filter(_.getType == Int32Type)
     val s2 = s20.filter(_.getType == Int32Type)
-    lexicographicDecreasing(s1, s2, strict = false, sizeOfOneExpr = bvSize)
+    lexicographicDecreasing(s2, s1, strict = false, sizeOfOneExpr = bvSize)
   }
 
 }

src/main/scala/leon/termination/StructuralSize.scala

@@ -14,8 +14,8 @@ import scala.collection.mutable.{Map => MutableMap}
 
 trait StructuralSize {
 
-  private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty
-  
+  private val sizeCache: MutableMap[TypeTree, FunDef] = MutableMap.empty
+
   /* Absolute value for BigInt type
    *
    * def absBigInt(x: BigInt): BigInt = if (x >= 0) x else -x
@@ -31,7 +31,25 @@ trait StructuralSize {
     absFun.typed
   }
 
-  /* Absolute value for Int (32 bit) type
+  /* Negative absolute value for Int type
+   *
+   * To avoid -Integer.MIN_VALUE overflow, we use negative absolute value
+   * for bitvector integers.
+   *
+   * def absInt(x: Int): Int = if (x >= 0) -x else x
+   */
+  val typedAbsIntFun: TypedFunDef = {
+    val x = FreshIdentifier("x", Int32Type, alwaysShowUniqueID = true)
+    val absFun = new FunDef(FreshIdentifier("absInt", alwaysShowUniqueID = true), Seq(), Seq(ValDef(x)), Int32Type)
+    absFun.body = Some(IfExpr(
+      GreaterEquals(Variable(x), IntLiteral(0)),
+      BVUMinus(Variable(x)),
+      Variable(x)
+    ))
+    absFun.typed
+  }
+
+  /* Absolute value for Int (32 bit) type into mathematical integers
    *
    * We use a recursive function here as the bv2int functionality provided
    * through SMT solvers is waaaaay too slow. Recursivity requires the
@@ -45,7 +63,7 @@ trait StructuralSize {
    *   1 + absInt(-(x + 1)) // avoids -Integer.MIN_VALUE overflow
    * }) ensuring (_ >= 0)
    */
-  def typedAbsIntFun: TypedFunDef = {
+  def typedAbsInt2IntegerFun: TypedFunDef = {
     val x = FreshIdentifier("x", Int32Type, alwaysShowUniqueID = true)
     val absFun = new FunDef(FreshIdentifier("absInt", alwaysShowUniqueID = true), Seq(), Seq(ValDef(x)), IntegerType)
     absFun.body = Some(IfExpr(
@@ -107,7 +125,7 @@ trait StructuralSize {
       case IntegerType =>
         FunctionInvocation(typedAbsBigIntFun, Seq(expr)) 
       case Int32Type =>
-        FunctionInvocation(typedAbsIntFun, Seq(expr))
+        FunctionInvocation(typedAbsInt2IntegerFun, Seq(expr))
       case _ => InfiniteIntegerLiteral(0)
     }
   }
@@ -129,6 +147,4 @@ trait StructuralSize {
       greaterBecauseGreaterAtFirstDifferentPos
     }
   }
-
-  def defs : Set[FunDef] = Set(sizeCache.values.toSeq : _*)
 }