Skip to main content

remove_implied_monotonic_constraints

foundry_evm_symbolic::runtime::solver::monotonic_product

Function remove_implied_monotonic_constraints 

Source 
pub(super) fn remove_implied_monotonic_constraints(
    constraints: Vec<SymBoolExpr>,
) -> Vec<SymBoolExpr>
Expand description

Removes hard-arithmetic comparisons implied by the remaining path constraints.

This keeps a sound monotonic success path from falling through to the heuristic witness search, whose satisfiable models are useful for counterexamples but cannot establish a proof.