Model-based program debugging exploits discrepancies between the program behavior anticipated by a programmer and the program’s actual behavior when executed on a set of inputs. From symptoms exhibited by a failing trace, potential culprits in the program can be localized. However, since the cause of the error is nested deeper into the code than the error itself, localizing errors and correcting the errors are most time consuming hard work. The error trace produced by a model checker may contain more information than it appears. Thus, counterexamples can be enough and are indicative for the cause of violation of the property. We present an assumption-based approach to localize the cause of a property violation using reasoning with constraints. In order to reduce the time consuming for error localizing, we first use dynamic program slicing to localize several statements to account for the violation of property. Assumption among these statements is then made to point out which statem...