Repository navigation
Can we remove "assertion failed" from successful assertions? #189
Description
Activity
Yes, I think these come specifically from
compiler/rustc_middle/src/mir/mod.rs.It is true that it may be confusing at times but RMC has nothing to do with this: the assertion text comes from MIR, the verification output comes from CBMC.
When viewing a CBMC trace from RMC, a user might see something like this:
The top assertion is failing and the bottom is provably true, but both have
assertion failed. I think this is just an artifact of how Rust proper prints assertions; it would be nice to remove this for CBMC usability.