search

epfl-lara / leon

The Leon system for verification, synthesis, repair
Other
162 stars 49 forks source link

Invalid methods actually compiles #312

Open Atry opened 7 years ago

Atry commented 7 years ago 
import leon.collection._ // for List
import leon.lang._       // for holds

object Example {
  def rightUnitAppend[T](l1: List[T]): Boolean = {
    l1 ++ Nil() == l1
  }.holds
}

In https://github.com/epfl-lara/leon/blob/master/src/sphinx/neon.rst

If you try to verify this last example you'll face a delicate situation: Leon runs indeterminately until it is either killed or times out. But why does this happen? The proposition doesn't seems more complicated than appendContent. Perhaps even more surprisingly, Leon is able to verify the following:

However, it actually compiles https://leon.epfl.ch#link/5cd42b18a4baeb936e2bd7ec996b90ab-1