* Temporary variables generated from `with` expressions
    should not be handled in the same way as normal variables,
    since we do not want Z3 to generate counter-examples by
    setting them to be different than the value bound at the
    `with` expression.

  * `With` expressions are necessary due to a main limitation of
    our intermediate logic language, namely that you can only
    put variables in certain places, rather than arbitrary
    expressions.

  * In the Z3 backend, this is now solved by "undoing" the
    intermediate with bindings, by unfolding them when we
    have converted LIR expressions to the AST of Z3 (which allows
    for arbitrary expressions in indexing, etc...

  * `docs/DEPLOY.md`: Deployment instructions

  * `docs/STRUCTURE.md`: File structure

  * Minor fixes in `README.md`, `Z3/API.hs`, `Normalizer.hs`

  * Deleted old `.gitmodules`

 * FIX problem with user-given real literals

 * EXTRA self-contained Z3 installation via the `install_z3.sh` script