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
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:
A failing VC we get looks like this:
A friendly error message would be something like: