ABSTRACT. We present a new safety hardware model checker SimpleCAR that serves as the “bottom-line” for evaluating and extending Complementary Approximate Reachability (CAR), a new SAT-based model checking framework inspired by classical reachability analysis. We demonstrate the performance of SimpleCAR on challenging benchmarks from the Hardware Model Checking Competition. Our experiments indicate that SimpleCAR is particularly suited for unsafety checking, or bug-finding; it is able to solve 7 unsafe instances within 1 hour that are not solvable by any other state-of-the-art technique, including BMC and IC3/PDR, within 8 hours. We also report 1 bug and 48 counterexample generation errors in the model checkers compared in our analysis.