Extraction of higher order function application fails
Extraction fails when using (+)
from int.Int
as an argument to a function.
a.mlw:
module Fail
use int.Int
let foo f = f 1 2
let test () = foo (+) (* extraction fails *)
end
module Ok
use int.Int
let foo f = f 1 2
let plus a b = (+) a b
let test () = foo plus (* extraction succeeds *)
end
why3 extract -L . -D ocaml64 a.Fail
fails with anomaly: Invalid_argument("index out of bounds")
while
why3 extract -L . -D ocaml64 a.Ok
succeeds.