MethodLifting reporting when subclasses have preconditions

[vkuncak]

MethodLifting creates a method in the superclass. When the methods in subclasses have preconditions, this causes a message that may be hard to understand. Take this example:

sealed trait IntList:
  def isEmpty: Boolean
  def head: Int   
  def tail: IntList

case class IntNil() extends IntList:
  def isEmpty: Boolean = true

  def head =
    require(false)
    ???

  def tail =
    require(false)
    ???

case class IntCons(head: Int, tail: IntList) extends IntList:
  def isEmpty: Boolean = false

A failing VC we get looks like this:

IntListHm.scala:4:7:   head     precond. (call head(({   assert(thiss.isInstanceOf[I... (require 2/2))  invalid           nativez3  0.0 
warning:  - Result for 'precond. (call head(({   assert(thiss.isInstanceOf[I... (require 2/2))' VC for head @4:7:
warning: thiss.isInstanceOf[IntCons]
IntListHm.scala:4:7: warning:  => INVALID
             def head: Int   
                 ^
warning: Found counter-example:
warning:   thiss: IntList -> IntNil()

A friendly error message would be something like:

require of IntList.head implies the require of IntNil.head