Automated Termination in Model Checking Modulo Theories