Kani and solver

[llooFlashooll]

Hi folks, I am very interested in this solid Kani Rust verifier work. I have some beginning questions that in the tutorial example https://model-checking.github.io/kani/tutorial-first-steps.html, there are many conditional branches.
I want to know the differences between Kani and symbolic execution, and how does Kani solve these conditional constraints? Thank you very much!

[zhassan-aws]

Hi @llooFlashooll. Thanks for your interest. Kani currently uses CBMC under the hood, which does use symbolic execution. Conditional constraints are resolved using a SAT solver.

[llooFlashooll]

I see. Thank you!