We present TRACER, a verifier for finite-state safety properties of se- quential C programs. It is based on symbolic execution (SE) and its unique fea- tures are in how it makes SE finite in presence of unbounded loops and its uses of interpolants to tackle the path-explosion problem.