Add integer synthesis

This pull request is meant for testing, comments, and discussion since it's using my own KLEE branch with experimental quantifier support. There will be many z3 timeouts, so try reducing the solver timeout to 3-5 seconds in sclang/sclang++.  Give it a try and let me know if you experience any problems. To enable synthesis, follow these instructions:

Remove third_party/klee and rerun `update_deps.sh`.
To enable iN synthesis, use z3 and add the `-souper-iN-synthesis`
cmd flag to the souper or set the `SOUPER_INT_SYNTHESIS` env variable
if you are using the sclang/sclang++ driver.

For some queries, z3 eats up the whole memory. Therefore, set the ulimits
and the `SOUPER_IGNORE_SOLVER_ERRORS` env var for the pass, e.g.,
```
ulimit -m 8000000
ulimit -v 8000000

export SOUPER_SOLVER="-z3-path=`which z3`"
export SOUPER_INT_SYNTHESIS=1
export SOUPER_IGNORE_SOLVER_ERRORS=1
```
These could be named parse*BitVector to emphasize that the functions are parsing only the bit vector token.