Demonstrates that Leon can be both unsound and incomplete because they use a table to model each unknown higher-order function.

LeonCounterexample.scala

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

object Test {
  
  /** Compute n's reciprocal, requiring n != 0 */
  def recip (n: Int): Int = {
    require (n != 0)
    1 / n
  }
  
  /** Contrived function taking higher-order inputs */
  def test(f: (Int => Int) => (Int => Int), g: Int => Int, h: Int => Int): Int = {
    recip (f(g)(1) + f(h)(2) + 3)
  }
  
  /** Suggested counterexample that turns out unsound */
  
  val f0 = (g: (Int) => Int) =>
    if (g == ((n: Int) => 1))
      (m: Int) => if (m == 2) -3 else -3
    else if (g == ((n : Int) => 1))
      (m: Int) => if (m == 1) 0 else 0
    else
      (m: Int) => if (m == 2) -3 else -3

  val g0 = (n: Int) => 1

  val h0 = (n: Int) => 1

  def falseCounterexample() = test(f0, g0, h0)
  
  
  /** Missed true counterexample */
  def missedCounterexample() = test (
    (_: (Int => Int)) => (n: Int) => if (n == 1) 0 else -3,
    (n: Int) => 0,
    (n: Int) => 0
  )
}