All-Values Symbolic Execution