The increasing cost of integrated circuits (IC) manufacturing has forced many design houses to become fabless. Outsourcing the stages of the manufacturing supply chain to the third-party facilities has introduced multiple forms of security threats. To combat these threats, amongst many design-for-trust countermeasure solutions, logic locking introduces the process of hiding the correct functionality of a circuit using key-programmable logic gates. However, the introduction of the satisfiability (SAT) attack has undermined the effectiveness of many existing logic locking solutions. Numerous resilient logic locking solutions have been introduced after the SAT attack to defend against the powerful SAT attack. In this seminar, after showing the shortcomings and limitations of the SAT attack, we introduce the Satisfiability Modulo Theory (SMT) attack on obfuscated circuits. The SMT attack is the superset of the Satisfiability (SAT) attack, with many extended capabilities and performance beyond the SAT attack. We demonstrate how the SMT attack uses one or more theory solvers in addition to its internal SAT solver to overcome the SAT attack limitations. For this reason, it is capable of modeling far more complex behaviors and could break the new logic locking techniques that are not breakable by the SAT attack. In addition, we describe the capability of the SMT attack in FOUR different variants: (1) we explain how SMT attack could be reduced to a SAT attack, (2) how the SMT attack could be carried out in Eager, and (3) Lazy approach, and finally (4) we introduce the Accelerated SMT (AccSMT) attack that offers significant speed-up to the SAT attack.