Abstract Interpretation of Symbolic Execution with Explicit State Updates