Saturn and Calysto scale their bit-precise analyses to large programs. With their design choices and techniques in mind, what do you suggest to improve the scalability of symbolic execution engines such as EXE/KLEE/DART/SAGE? How do you expect your suggestion to affect the attainable results?