Satisfiability Modulo Theories (SMT) solvers are fundamental tools for program analysis and verification. The satisfiability problem for first-order logic is undecidable. In practice, SMT solvers typically employ various heuristics and are inherently incomplete. Solvers return \(\textsf{unknown}\) if they cannot solve a particular formula. The \(\textsf{unknown}\) results drastically hinder the usability of SMT solvers and directly affect client applications. The standard way to reduce \(\textsf{unknown}\) cases is to develop more powerful solvers, which requires significant algorithmic and engineering efforts. This work-in-progress paper discusses a new perspective on improving SMT solving: instead of developing more powerful solvers for all formulas, we focus on mutating “hard” formulas ( \(\textsf{unknown}\) formulas) to make them “easier” to solve. That gives us enormous flexibility to process \(\textsf{unknown}\) formulas without affecting normal formulas. Specifically, given an \(\textsf{unknown}\) formula and a solver, we propose to repeatedly modify the formula via structural mutations. Our key insights are (1) structural mutations make formulas smaller so that they are presumably easier to reason about, and (2) structural mutations approximate formulas so that we can reason about the original formulas indirectly. Then, we utilize the same solver to solve the mutated formulas to retrieve the \(\textsf{sat}\) / \(\textsf{unsat}\) results of the original \(\textsf{unknown}\) formulas.