While registering transfer level or even behavioral level, the hardware description language is widely used, and Satisfiability Modulo Theories(SMT) gradually replaces Boolean Satisfiability(SAT), and plays an important role in VLSI formal verification. A minimal unsatisfiable subformula can help automatic tools to rapidly locate the errors. A depth-first-search algorithm is proposed to extract minimal unsatisfiable subformulae in SMT to adopt depth-first searching and incremental solving strategy. The experimental results show that the depth-first-search algorithm effectively derived minimal unsatisfiable subformulae, and is more efficient than the breadth-first-search algorithm, which is the best method for computing the minimal unsatisfiable subformulae in SMT, with the number of variables and clauses in the original formulae increasing.