## 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 SMT formula. Or one function as in Veritesting.

12 pages

Sergey Vartanov, 2007–2020