XXX beginnings of a translation to SMV

This is based on `murphi2uclid`. But unlike Uclid5 translation, this is much
more rough. The semantics and structure of SMV are sufficiently different that
an automatic translation would be more like a compiler than the AST-walking
strategy employed by the `murphi2*` tools. It does not seem worth undertaking
something this ambitious until we get some experience in whether this
translation is useful.