Symbolic execution with existential second-order constraints