1. A method for analyzing a software program, said method comprising the steps of: receiving input constraints for a path in said software program to be feasible; applying one or more rewrite rules to a flow graph of said software program defining how said flow graph can change; adding at least one new node or new edge to said flow graph based on said rewrite rules; deriving new constraints by arithmetic constraint solving from said input constraints, said flow graph and one or more existing constraints; and adding said one or more new constraints to said existing constraints.