Synthesize solving strategy for symbolic execution