Automated reasoning is at the core of many verification tasks and is widely used in industrial settings. I will discuss difficulties solving non-linear constraints over transcendental functions, traditional approaches, and in particular I will present the ksmt calculus, why it provides a \delta-complete procedure for that task when functions are computable, potential extensions of it to other domains, as well as open problems in this area.