NULL is a value too for the sake of unused local variable elimination
NULL is a value too for the sake of unused local variable elimination

FStarLang/kremlin,FStarLang/kremlin,FStarLang/kremlin,FStarLang/kremlin