We present a comparison of a traditional method, as implemented in a popular compiler, and one utilizing translation to quantifier-free fixed-size bit-vector logic (QF_BV). Accuracy and run time of each approach has been assessed, and in some cases the SMT method has been found to produce surprising, but nonetheless correct results. A combination of both approaches is proposed, focusing on the strengths of each method.
Comparative study on compiler optimization
Benchmark the experimental results against GCC compiler
Discuss future work