Excluding bound variables of match expressions when computing free variables

[amaurremi]

When we compute the free variables of an expression we need to exclude its bound variables. At the moment, the computation of the free variables of an expression only excludes bound variables of "comprehension" expressions (which include lambdas, forall statements, etc.) but does not take into account the bound variables that can be introduced in the cases of pattern matching. This PR fixes this.

@RustanLeino @samuelgruetter

[amaurremi]

This bug manifested itself when compiling the StateMonad.dfy test without the compile:0 option, resulting in a runtime exception. I now disabled that option, so the extensive pattern matching in the state-monad test serves as a test case for this fix.