SMT: use a name mangling scheme based on identifiers instead of names

Instead of translating a variable like "foo" into something like "ru_foo" in the
SMT bridge, we translate it to something like "s23". The purpose of this is to
support symbol shadowing. E.g. in Murphi you can declare a rule-local variable
that shadows one of the state variables. In translation to SMT this previously
resulted in a malformed problem with a duplicate symbol definition.

It would have been possible to work around this using scoping in SMT (`push` and
`pop` commands) but these are not supported by all solvers. Instead we stop
relying on the uniqueness of the Murphi symbols and construct unique symbols out
of the AST identifiers. This makes the SMT problem less readable but more often
syntactically well formed.

Note that a side effect of this change is that Murphi identifiers that use
characters not understood by your SMT solver (e.g. UTF-8 accented letters) no
longer cause malformed SMT problems.

Github: closes #151 "variable shadowing causes invalid SMT problems"