const unique LOC_ID: int;
axiom LOC_ID == 0;