```c int z; void f () { z = 0; } ``` Gives: ```fstar fn f () { z := 0l; } ``` With a non-existing `z`. At least, we should properly raise a translation error if we find references to global mutable variables. We should discuss how to actually support it.