src/Tools/SML/Example.sml

prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas

structure Example :> Example =
struct

type t = int

val a = 0
fun b x = x + 1

end