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 unknown if they cannot solve a particular formula. The unknown results drastically hinder the usability of SMT solvers and directly affect client applications. The standard way to reduce 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 (unknown formulas) to make them “easier” to solve. That gives us enormous flexibility to process unknown formulas without affecting normal formulas. Specifically, given an 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 sat/unsat results of the original unknown formulas.