Skip to main content

check_certificate

foundry_evm_symbolic::runtime::solver::reasoning::xor

Function check_certificate 

Source 
fn check_certificate(
    relations: &[Relation<'_>],
    sources: U256,
    disequality: Option<usize>,
) -> bool
Expand description

Checks a contradiction certificate by XORing selected source equalities directly. All opaque terms must cancel, leaving 0 = nonzero, or 0 != 0 for a disequality certificate. This is a necessary contradiction even when atoms are related (e.g. x and x & mask); no independence assumption is used to establish UNSAT.