Skip to main content

normalize_sat_constraints

foundry_evm_symbolic::runtime::solver

Function normalize_sat_constraints 

Source 
fn normalize_sat_constraints(
    cx: &mut SymCx,
    constraints: &[SymBoolExpr],
) -> Vec<SymBoolExpr>
Expand description

Normalizes satisfiability constraints and removes soundly implied nonlinear comparisons.