Can we not introduce a dirty hack into the formal specification solely to work around an edge case introduced by another dirty hack that's already in the formal specification?