Empty preconditions error

[TheDeveloper101]

Attempting to convert programs with an empty preconditions gives the following error: Every statement in invariant block must be a pure boolean invariant.

Minimal test case for reproducing the error:

fun f(Int a): Int{ preconditions { } return a; }