Function preconditions and postconditions do not propagate across module boundaries and crash the compiler

[Stef-2]

I wrote a minimal demo here.
contract_assert() works fine, which I'm assuming is because it is a assert() / [[assume()]] in disguise.
All three work fine when used in regular header files. I have not tested header units.