A system, method and computer program product to refine an original complex CFG into a simpler CFG showing interesting paths and reducing interfering paths with dynamic input for the state of program. The method receives/encodes dynamic user input in the form of annotations which encodes user's special interests or knowledge of the program at run time, e.g., some assumptions of any variables appeared, which can be equations of variable and value or relationships between variables. The method then simplifies all the branching points in a generated AST (Abstract Syntax Tree) whenever possible by querying a SMT (Satisfiability Modulo Theories) solver with branching condition and the user annotations and by evaluating immediate values of expressions or eliminate unreachable parts in the CFG. Finally, the method generates a simplified CFG by simplified AST. This can assist a programmer to understand the code and facilitates correlating different basic blocks under a same scenario.