Verification tasks that need to consider loops with non-static loop bound. Contributed by the ESBMC project.