Multiplex Symbolic Execution: Exploring Multiple Paths by Solving Once