Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis