> > Thank you very much. I was turning endlessly in the website > without finding that. I now have some stuffs to read. As far as I can tell, Z3 is an SMT solver (Satisfiability Modulo Theories), which is a SAT Solver an steroids.