The SMT encoding documentation needs to be updated: - [upstream](https://github.com/kframework/k/blob/master/pending-documentation.md#smt-lemma-lemma-and-trusted-attributes), and - in the [design decisions](https://github.com/kframework/kore/blob/master/design-decisions/2018-11-05-Translating-predicates.md) by making a document which reflects the _current state_ of SMT encoding.