Quantifier-free encoding of hybrid systems with non-linear dynamics