Solvers don&#x27;t do brute force at all. Otherwise you wouldn&#x27;t come up with ways to crack crypto. Solvers work with SAT and SMT languages, which means purely logical and extended to simple words and bitarrays, and the solvers mentioned there (cbmc is also in this league), can solve normal programming logic backwards.<p>Means you assert a result on a variable at the end, specify which variables and states will affect the wanted result, and the framework and solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by filtering out impossible paths and values. Like in a game.<p>Z3 is very popular, because you can write your problem in python. 
Ages ago lisp was very popular, and some of the very first lisp programs from the 60ies were such solvers (general planner) leading to AI. 
And recently with the implementation of efficient simple open-source SMT solvers (minisat, ...) implemented within gcc or llvm you can now even use normal C programs and backtrack results, optimize and check types, do bounds checking, generate tests from bugs and so on. This is not comparable to simple fuzzing or brute-forcing, it knows the program flow, and works the flow backwards.