Resurrect extraction of `prover`
The code in examples/prover
is supposed to be extractable to OCaml. However its extraction is not tested by the bench. Even worse, its extraction currently triggers an unexpected error:
cd examples/prover
make BENCH=yes
why3 -L . --debug=ignore_unused_vars extract -D ocaml64 -o prover.ml ProverTest.mlw
File "./Unification.mlw", line 887, character 8 to line 929, character 13:
Compiler error: tuple <> unification_return()