## 1 Introduction  
The symbolic execution technique can effectively find vulnerabilities in a program by testing each state of the program. Due to this advantage, symbolic execution techniques are widely used in competitions such as \"Capture The Flag\" (CTF) to analyze the execution state of the target program and try to discover vulnerabilities in it. Although the basic blocks of a program are finite during static analysis, the state space in most programs during dynamic execution is infinite. This leads to that symbolic execution is often used in small, simpler test programs, such as CTF. In the case of complex programs that people actually use in their daily lives, such infinite states will make it difficult for symbolic execution to discover potential vulnerabilities in the program. At the present stage, symbolic execution appears mainly as an assistant tool in vulnerability discovery. It is widely used in hybrid-fuzzing as a supplement to fuzzing. [PERSON] [1] provides a simple hybrid fuzzing idea. It introduces symbolic execution as an assist to improve the coverage of vulnerability discovery when fuzzing is difficult to improve its coverage. QSYM [2] focuses on making symbolic execution more suitable for hybrid fuzzing usage cases. SAVIOR [3] proposes a bug-driven hybrid fuzzing approach. It focuses more attention on the parts of the code that have bugs by the undefined behavior sanitizer. HFL [4] improves the applicability of hybrid fuzzing and introduces hybrid fuzzing into kernel vulnerability discovery. Symbolic execution could have provided more contributions to the vulnerability discovery. However, infinite states seriously limit the applicability of symbolic execution. Therefore, this paper proposes a multi-priority path exploration strategy based on abstract syntax tree (AST) analysis to mitigate the impact of these infinite states on the applicability of symbolic execution techniques. We designed and implemented EtWExplorer, a multi-priority scheduling path exploration technique based on abstract syntax tree analysis. First, we identified the symbolic expressions generated in the program and recorded them. Then, we identified the constraints that could not be satisfied in the program and formed a correspondence between these unsatisfiable constraints and the identified symbolic expressions. When a basic block was repeatedly analyzed, we determined whether the symbolic expressions generated by the current basic block were related to the unsatisfiable constraints. Moreover, according to the corresponding analysis results, the basic blocks were classified into different priorities (this allows more meaningful program states to be executed with higher priority, while less meaningful program states will have lower priority). Thus, the impact of the state space explosion on symbolic execution was mitigated. Then, we can more easily explore the unknown paths in the program. In summary, this paper contributes the following:  
We analyzed that the cause of the state space explosion during symbolic execution was the massive growth of the state space caused by branching during repeated code execution. How to determine whether repeated code should be symbolically executed is the key problem to solving the state space explosion. We propose an abstract syntax tree analysis approach that analyzes the positive direction of specific expressions in unsatisfied constraints. With the obtained positive direction, we can effectively classify the states generated in the symbolic execution with multiple priorities to mitigate the state space explosion in path exploration. We designed a new path exploration technique. It analyzes the symbolic expressions generated in the program to prioritize the states generated in the symbolic execution. Ultimately, this prioritization is used to enhance the path exploration capability of symbolic execution. We implemented the prototype tool EtWExplorer for the proposed multi-priority scheduling algorithm based on the abstract syntax tree analysis.