Connect to GDB
AbstractGDB has a client/server system to allow the debugger to be controlled from other programs. It would be awesome to have a feature for CBMC that allows a trace to be run via gdb. This would allow easy integration with existing debugging tools (an IDE plug-in could simply drop the programmer into the debugger with an execution trace that causes the problem), some really cool CEGAR like tricks and some fun with parallel programs using multiple debuggers / the thread support and possibly reverse debugging to allow error traces to be explored.
To do this will require working out which functions are non-deterministic models of real functions and accounting for this. This would also be necessary for some of the preceeding ideas.