Scalable and precise verification based on k-induction, symbolic execution and floating-point theory