Z3 fixes

This adds support for `!=` when using Z3. It also fixes a bunch of issues I encountered when using it. In theory it should pass, but Travis shows some error. I cannot access the logs from here, @onsetsu, can you check it out?