Abstract serves as an automatic test generation tool designed for C programs based on symbolic execution. employs fuzzing-based pre-analysis and combines static symbolic execution and dynamic symbolic execution to improve the effectiveness of test generation. achieves 5132 scores and is ranked 4th in the branch coverage track of Test-Comp 2024.

Array constraint solving is widely adopted by the existing symbolic execution engines for encoding programs precisely. The counterexample-guided abstraction refinement (CEGAR) based method is state-of-the-art for array constraint solving. However, we observed that the CEGAR-based method may need many refinements to solve the array constraints produced by the symbolic executor, which decreases the performance of constraint solving. Based on the observation, we propose a machine learning-based method to improve the efficiency of the CEGAR-based array constraint solving. Our method adaptively turns on or off the CEGAR loop according to different solving problems. We have implemented our method on the symbolic executor KLEE and its underlying CEGAR-based constraint solver STP. We have conducted an extensive experiment on 55 real-world programs. On average, our method increases the number of explored paths by 21%. The results of the extensive experiments on real-world C programs show the effectiveness of our method.