1. A method for detecting infeasible paths in a program, comprising: performing a path-insensitive abstract interpretation to generate invariants that hold true in program locations; projecting said invariants along all paths to other program locations; enumerating a set of combinations of the projected invariants by generating subsets of the projected invariants that correspond to locations in continuous path segments in the program and checking the enumerated combinations to determine whether their conjunctions are logically false using a Boolean satisfiability solver and a theory-satisfiability solver in combination; and if an enumerated combination is checked and found to having a logically false conjunction, determining that an associated set of paths is infeasible.