Systems and methods for SMT processes using uninterpreted function symbols. A method includes receiving a configuration model. The method includes computing a variant for the configuration model that includes a non-linear function. The method includes identifying input/output pairs in the non-linear function of the variant. The method includes executing a process on an external application for each input/output pair to produce an output value corresponding to each input of the input/output pairs. The method includes comparing the output value corresponding to each input of the input/output pairs with the output corresponding to each input of the input/output pairs. The method includes, when the output value corresponding to each input of the input/output pairs is equal to the output corresponding to each input of the input/output pairs, then the system stores an indication that the variant is correct.