Application of SMT solvers to hybrid system verification