Function path_predicate 

fn path_predicate(
    gcx: Gcx<'_>,
    expr: &Expr<'_>,
) -> Option<(PathPredicate, bool)>

The boolean fact expr establishes when it evaluates to true: a local flag, its negation, or an ==/!= between locals and literals.