Filling DP table in order

orderedFill.scala

package wihtOrb

import leon._
import mem._
import lang._
import annotation._
import com.sun.xml.internal.bind.v2.runtime.reflect.Lister.Pack
import instrumentation._
import invariant._

object orderedFill {
  
  def fillTable(i: BigInt, j: BigInt, m: BigInt, n: BigInt): BigInt = {
  	require(i >= 0 && j >= 0 && m >= i && n >= j)
	  if (i == m && j == n) 
	  	BigInt(0)
	  else if(j == n)
	    fillTable(i + 1, 0, m, n) 
	  else  
	    fillTable(i, j + 1, m, n)
  } ensuring (time <= ? * (m - i) * n + ? * (n - j) + ?)

}

? * (expr) is extracted differently. So it will work

However, the benchmark still doesn't work. Try increasing UNROLL_BOund in the file leon.invaraint.engine.RefinementEngine