\emph{Symbolic execution/} is an important program analysis technique that provides auxiliary execution semantics to execute programs with symbolic rather than concrete values. There has been much recent interest in symbolic execution for automatic test case generation and security vulnerability detection, resulting in various tools being deployed in academia and industry. Nevertheless, (subtype or dynamic) polymorphism of object-oriented programs has been neglected: existing symbolic execution techniques can explore different targets of conditional branches but not different targets of method invocations. We address
the problem of how this polymorphism can be expressed in a symbolic execution framework. We propose the notion of \emph{symbolic types/}, which make object types symbolic. With symbolic types, \emph{various targets of a method invocation can be
explored systematically} by mutating the type of the receiver object of the method during automatic test case generation.
To the best of our knowledge, this is the first attempt to address polymorphism in symbolic execution. Mutation of method invocation targets is critical for effectively testing object-oriented programs, especially libraries.
Our experimental results show that symbolic types
are significantly more effective than existing symbolic execution techniques in achieving test coverage and finding bugs and security vulnerabilities in \code{OpenJDK}.