&gt;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.<p>Any links to examples of the above?