One of the primary challenges in software testing is the generation of high-quality test inputs and the acquisition of corresponding test oracles. This paper introduces a novel methodology to mitigate this challenge in testing program verifiers, employing SMT (Satisfiability Modulo Theories) formulas as a universal test case generator. The central concept is converting SMT formulas into programs, while maintaining their safety consistency. This conversion links the formulas’ satisfiability with the programs’ safety properties, allowing the former’s satisfiability to act as an oracle for program verifiers. This method was implemented as a framework named SMT2Test, which facilitates the transformation of SMT formulas into Dafny and C programs. An Intermediate Representation was developed to augment this framework’s flexibility, streamlining the conversion for other programming languages and fostering general, modular transformation strategies. The effectiveness of SMT2Test was evaluated by applying it to find bugs in two program verifiers: the Dafny verifier and CPAchecker. Utilizing the SMT2Test framework, we discovered and reported a total of 14 previously unknown bugs that were not found by previous methods. After reporting, all of them have been confirmed, and 6 bugs have been fixed. These findings show the effectiveness of our method and imply its potential application in testing other programming language infrastructures.