added special flag for scwala path budget
fixed soundness bug arising in very rare cases when we have two symbolic LHS's that might match, but no local binding for one of the LHS's