z3 times out on an example program with Strings, succeeds with BigInts

[drganam]

For the following example, Stainless times out with z3. After replacing Strings with BigInts, it finds a counterexample:

m: Lambda -> C(C(V(BigInt("8")), V(BigInt("8"))), P(BigInt("8"), V(BigInt("8"))))

import benchmarks_lambda_defs._
import stainless.collection._
import stainless.lang._
import stainless.annotation._

object benchmarks_lambda_defs {
  sealed abstract class Lambda {}
  case class V(param0: Var) extends Lambda {}
  case class P(param0: Var,  param1: Lambda) extends Lambda {}
  case class C(param0: Lambda,  param1: Lambda) extends Lambda {}
  
  type Var = String // BigInt
}

object I_lambda_sub5 {

  def check(m: Lambda): Boolean = {
    def make_area_list(m: Lambda): List[Var] = {
      m match {
        case V(n)      => { Nil() }
        case P(n, m1)  => { n :: make_area_list(m1) }
        case C(m1, m2) => { make_area_list(m1) ++ make_area_list(m2) }
      }
    }
    def match_list_with_station(m: Lambda, l: List[Var]): Boolean = {
      m match {
        case P(n, m1) => { match_list_with_station(m1, l) }
        case C(m1, m2) => {
          match_list_with_station(m1, l) && match_list_with_station(m2, l)
        }
        case V(n) => { if (l.exists((x: Var) => { x == n })) true else false }
      }
    }
    match_list_with_station(m, make_area_list(m))
  }

  def check5(m: Lambda): Boolean = {
    def check55(env: List[Var], m: Lambda): Boolean = {
      m match {
        case P(var0, m_0) => { check55(var0 :: env, m_0) }
        case C(m1, m2) => { 
          val e1v = check55(env, m1)
          val e2v = check55(env, m2)
          e1v && e2v
        }
        case V(var0) => { env.exists((t) => { t == var0 } ) }
      }
    }
    check55(Nil(), m)
  }

  def eq(m: Lambda) = {
  } ensuring (check5(m) == check(m))

}

[mario-bucev]

Tested with CVC4 as well, it also times out! I'll delve into this issue this Friday & during the WE if that's fine for you.

[drganam]

Ah true, I forgot to mention CVC4: it times out for reasonable timeouts indeed, but eventually (timeout=500) finds this counterexample: Lambda -> C(C(V(""), V("")), P("", V("")))