Macro crucible_assert 

macro_rules! crucible_assert {
    ($cond:expr) => { ... };
    ($cond:expr, $fmt:expr) => { ... };
    ($cond:expr, $fmt:expr, $($args:tt)*) => { ... };
}

Assert that a condition holds. During symbolic testing, crux-mir will search for an assignment to the symbolic variables that violates an assertion.

This macro works just like the standard assert!, but currently produces better error messages.

If the error message uses string formatting, crux-mir will choose an arbitrary concrete counterexample and use its values when formatting the message. For example, crucible_assert!(x + y == z, "bad arithmetic: {} + {} != {}", x, y, z); might print a message like bad arithmetic: 1 + 2 != 4, assuming x, y, and z are symbolic variables that can take on the values 1, 2, and 4..