Towards better simplifications in SMT solvers with applications in string solving