We present Soteria Rust, a symbolic execution engine for Rust built using Soteria, a symbolic execution library for OCaml. Soteria Rust is the first symbolic execution engine for Rust that supports checking for bugs related to Tree Borrows. Thanks to Soteria’s modular design, we were able to implement the engine in 8 person-months, resulting in a competitive engine that is more semantically accurate than Kani, while also being an order of magnitude faster on some examples. We present the high-level design of the engine, and follow by a comprehensive evaluation of Soteria Rust against both Kani and Miri, Rust’s official concrete interpreter. Finally, We also discuss some techniques to improve the performance of the usage of SMT solvers, notably applied to symbolic execution. To this end, we use techniques inspired from abstract interpretation, porting them to a UX context.