The expressiveness of LLVM IR is very close to C. Given a high enough tolerance for pain, one could implement the same rewrite that the rust compiler would impl

The expressiveness of LLVM IR is very close to C. Given a high enough tolerance for pain, one could implement the same rewrite that the rust compiler would implement in C (without even going into inline assembly). In practice… maybe. However, I find we're more forgiving of unpredictable performance (either wrt analysis runtime or quality of analysis) in safety checking tools than in code generators. The ergonomics of bitblasting code generation questions to SAT aren't great.