We will add support to model checking engeines portfolio for Kani by adding one new model checking engine, which will allow users to verify code that CBMC currently fails to verify in a reasonable time. Users will be able to choose a specific engine to run on each harness or to just run all engines in parallel until one finishes. This will enable users to use Kani to verify more complex harnesses and code that they couldn’t verify otherwise.