Evaluator crash

[vkuncak]

The --eval crashes on list2 evaluation inside the ++ method.

object ScalaList:
  sealed abstract class List[+A]:
    def :: [B >: A](elem: B): List[B] =  Cons(elem, this)

    def ++[B >: A](that: List[B]): List[B] =
      this match
        case Nil => that
        case Cons(a, as) => a :: (as ++ that)

    def tail: List[A] =
      require(this != Nil)
      this match
        case Cons(a, as) => as

    def head: A = 
      require(this != Nil)
      this match
        case Cons(a, as) => a
  end List

  case object Nil extends List[Nothing]
  final case class Cons[+A](first: A, next: List[A]) extends List[A]

  def list: List[Int] = Cons(10, Cons(20, Cons(30, Nil)))
  def list2: List[Int] = list.++[Int](list)
end ScalaList

[vkuncak]

Still crashing as of Version: 0.9.7-21-gf95184b

[mario-bucev]

After TypeEncoding, we get for ++:

def ++$2(A$124: (Object$0) => Boolean, B$80: (x$122: Object$0) => { b$20: Boolean | ((A$124(x$122) ==> b$20)): @dropConjunct  }, thiss$4: { x$123: Object$0 | (isList$0(x$123, A$124)): @dropConjunct  }, that$19: { x$125: Object$0 | (isList$0(x$125, B$80)): @dropConjunct  }): { x$127: Object$0 | (isList$0(x$127, B$80)): @dropConjunct  } = {
  thiss$4 match {
    case Nil$2() =>
      that$19
    case Cons$2(a$24, as$1) =>
      ::$3(B$80, B$80, ++$2(A$124, B$80, as$1, that$19), a$24)
  }
} ensuring {
// This postcondition is added by TypeEncoding relating ++$2 (this definition) with ++$3 (choose variant)
  (res$44: { x$127: Object$0 | (isList$0(x$127, B$80)): @dropConjunct  }) => 
    ((res$44 == thiss$4 ++$3 that$19)): @dropConjunct 
//                      ^^^^
//                 choose variant
}

@derived(++$2)
def ++$3(thiss$8: Object$0, that$20: Object$0): Object$0 = choose$3(thiss$8, that$20)

@derived(++$3)
@DropVCs
def choose$3(thiss$13: Object$0, that$21: Object$0): Object$0 = choose(((res$49: Object$0) @DropVCs) => true)

When --eval runs, after evaluating ++, it checks that the postcondition holds.
For the last recursive call, it checks whether Cons(10, Cons(20, Cons(30, Nil))) == Nil() ++$2 Cons(10, Cons(20, Cons(30, Nil))).
Here it will use ++$2 (the choose variant) which will return the simplest possible value, that is, Nil().
So we get Cons(10, Cons(20, Cons(30, Nil))) == Nil() which does not hold.
Passing the --ignore-contracts flag makes the evaluation succeed.

However, since the postcondition is only there to help verification and is not supposed to be verified (due to being annotated with @dropConjunct), I'd argue that the evaluator should skip the evaluation.