Error metrics are used to evaluate the quality of an approximated circuit or to trade-off several approximated candidates in design exploration. Precisely determining the error or all approximated circuit is a hard problem since the errors accumulate over time depending on the composition and nature of individual components. In this paper, we present methods based on model checking to precisely determine error behavior in sequential circuits that contain approximated combinational components. Our experiments show that such an analysis is very significant and crucial to properly deduce the effects of approximations.