fn remove_witnessed_isolated_hash_constraints(
cx: &mut SymCx,
constraints: Vec<SymBoolExpr>,
) -> Vec<SymBoolExpr>Expand description
Removes independently satisfiable constraints over one opaque hash symbol.
SMT treats symbolic hashes as free bit-vector symbols. If a constraint’s only SMT symbol is a hash unused by other constraints, a concrete witness proves that it cannot affect conjunction satisfiability. The witness is discarded because hash values are not replayable inputs.