This file demonstrates a seemingly bug in the Leon verifier

BraunTree.scala

import leon.lang._
import leon.lang.synthesis._
import leon.annotation._

object BraunTree {
  sealed abstract class Tree
  case object Leaf extends Tree
  case class Node(l: Tree, n: Int, r: Tree) extends Tree
  
  def size(t: Tree): Int = t match {
    case Leaf => 0
    case Node(l, _, r) => 1 + size(l) + size(r)
  }
  
  def isBraunTree (t: Tree): Boolean = t match {
    case Leaf => true
    case Node(l, n, r) =>
      val nl = size(l)
      val nr = size(r)
      isBraunTree(l) && isBraunTree(r) && (nl == nr || nl == 1 + nr)
  }
  
  // Normal "weak" insert without pre/post conditions
  def weakInsert(t: Tree, x: Int): Tree = t match {
    case Leaf => Node(Leaf, x, Leaf)
    case Node(l, v, r) => Node(weakInsert(l, x), v, r)
  }
  
  // Wrap "weak" insert with pre/post conditions
  def wrappedInsert(t: Tree, x: Int): Tree = {
    require (isBraunTree(t))
    weakInsert(t, x) ensuring (isBraunTree(_))
  }
  
  // couterexample triggering `wrapInsert`'s post-condition failure
  val booYa: Tree = wrappedInsert(Node(Node(Leaf, 0, Leaf), 0, Leaf), 0)
  
  // "Strong" insert with pre/post condition
  def strongInsert(t: Tree, x: Int): Tree = {
    require (isBraunTree(t))
    t match {
      case Leaf => Node(Leaf, x, Leaf)
      case Node(l, v, r) => Node(strongInsert(l, x), v ,r)
    }
  } ensuring (isBraunTree(_))
}