We present an algorithm and implementation for the bounded verification or testing of heap-manipulating programs in pursuit of safety properties. This algorithm is based on symbolic execution whose exploration covers every execution path up to a certain length. The novel feature is the use of symbolic heaps in order to precisely model the effect of dynamic memory allocation, and critically, the use of property-directed interpolation in order to obtain a useful relaxation of the path constraints. In other words, we perform dynamic symbolic execution with pruning. Finally, we describe our implementation TRACER-X and present an experimental evaluation against LLBMC, a state-of-the-art system for bounded verification, and KLEE, a state-of-the-art dynamic symbolic executor used for testing.