Symbolic execution is a technique to analyze a binary. It symbolizes the input ofa program and try to generate testcases that covered all of the feasible path. Theconstraint solver is one of the indispensable and the most critical components in asymbolic execution engine. All of the symbolic execution engines rely on solvers toconduct testcases and guide the exploration during the operation process that issolving constraints that are collected during the execution process. Currently, andengine regularly spends comparatively long time solving the constraints. To shortenthe time for analyzing a binary, using a standalone solver is one of the practicalstrategies. In my research, I implemented a standalone solver that takes in kquerystringsandgeneratingtestcasesaccordingtotheconstraintsinthatkqueryitreceives.Moreover, to improve the performance of the solver, I decided to let the solver sharecaches. If the kquery string is solved before, it is unnecessary to solve it again.
