LLVM Optimizations with KLEE

[rafaelsamenezes]

Is your feature request related to a problem? Please describe.
Not related to a problem. Currently, we default to -O3 optimizations and let KLEE decides which solver to be used. The -O3 may not be the best for Symbolic Execution and the SMT formula generated by KLEE may not be the best for the selected solver.

Describe the solution you'd like
We should select which solver and the best optimization for Symbolic Execution.

Describe alternatives you've considered
Extend Map2Check to have a class to select which optimizations will be done.

Additional context
The paper Studying the influence of standard compiler optimizations on symbolic execution contains details on how LLVM optimizations affects KLEE and the solvers