GitLab

Extraction of absurd is currently assert false which is perfectly fine. Though, during development it happens that absurd is temporary used on "todo" branches as one uses assert false in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting

# <line number> <mlw file name>

on the line before assert false