Path Selection for Symbolic Execution and Variable Selection for Constraint Solving