Efficient State Merging in Symbolic Execution
1 If you have program if (x < 0) x = 0; else x = 5; with X assigned to x you can merge two states (X < 0, [x = 0]) and (X >= 0, [x = 5]) to one state (true, [x = ITE(X < 0, 0, 5)]). So, you can represent whole program with one . Or one function as in .
Sergey Vartanov, 2007–2020