re14: Fix bugs with new encoding

* Turn n into no
* Fix label optimization when a node name is not explicitly declared in
the z3 model