google/souper — pull request #108 by rsas (2014-11-05 22:17:09+00:00)
Title: 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 to 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
```