Function normalize_constraints_for_solver 

pub(crate) fn normalize_constraints_for_solver(
    cx: &mut SymCx,
    constraints: &[SymBoolExpr],
) -> Vec<SymBoolExpr>

Normalizes path constraints into an equivalent, solver-friendlier form.