We discuss how to solve reachability problems either in BDD based symbolic model checking (by NuXMV) or by bounded model checking using SMT solving. We provide several examples, mainly from the practical assignments of the course Automated Reasoning, over the years. These include deadlock checking in hardware and infinite branching.
