StackOverflowError during Measure Inference

[drganam]

When running the termination check for the following program, Stainless crashes with a stack overflow error:

import stainless.lang._

object C_formula_sol338 {

  sealed abstract class Formula {}
  case object True_ extends Formula {}
  case object False_ extends Formula {}
  case class Not(param0: Formula) extends Formula {}
  case class AndAlso(param0: Formula, param1: Formula) extends Formula {}
  case class OrElse(param0: Formula, param1: Formula) extends Formula {}
  case class Imply(param0: Formula, param1: Formula) extends Formula {}
  case class Equal(param0: Exp, param1: Exp) extends Formula {}

  sealed abstract class Exp {}
  case class Num(param0: Int) extends Exp {}
  case class Plus(param0: Exp, param1: Exp) extends Exp {}
  case class Minus(param0: Exp, param1: Exp) extends Exp {}

  def cal_exp(n: Exp): Int = {
    n match {
      case Num(a) => { a }
      case Plus(e1, e2) => { cal_exp(e1) + cal_exp(e2) }
      case Minus(e1, e2) => { cal_exp(e1) - cal_exp(e2) }
    }
  }

  def eval(f: Formula): Boolean = {
    f match {
      case True_ => { true }
      case False_ => { false }
      case Not(x) => {

        val v = eval(x)
        v match {
          case true => { eval(False_) }
          case false => { eval(True_) }
        }

      }
      case AndAlso(e1, e2) => {

        val v1 = eval(e1)

        val v2 = eval(e2)
        (v1, v2) match {
          case (true, true) => { eval(True_) }
          case (true, false) => { eval(False_) }
          case (false, true) => { eval(False_) }
          case (false, false) => { eval(False_) }
        }

      }
      case OrElse(e1, e2) => {

        val v1 = eval(e1)

        val v2 = eval(e2)
        (v1, v2) match {
          case (true, true) => { eval(True_) }
          case (true, false) => { eval(True_) }
          case (false, true) => { eval(True_) }
          case (false, false) => { eval(False_) }
        }

      }
      case Imply(e1, e2) => {

        val v1 = eval(e1)

        val v2 = eval(e2)
        (v1, v2) match {
          case (true, true) => { eval(True_) }
          case (true, false) => { eval(False_) }
          case (false, true) => { eval(True_) }
          case (false, false) => { eval(True_) }
        }

      }
      case Equal(e1, e2) => {

        val v1 = cal_exp(e1)

        val v2 = cal_exp(e2)
        (v1, v2) match {
          case (v1, v2) => { if (v1 == v2) eval(True_) else eval(False_) }
        }

      }
    }
  }
}