Skip to main content

fallback_bounded_model

foundry_evm_symbolic::runtime::solver::fallback

Function fallback_bounded_model 

Source 
pub(crate) fn fallback_bounded_model(
    constraints: &[SymBoolExpr],
) -> Option<HashMap<Symbol, U256>>
Expand description

Searches a bounded Cartesian portfolio and returns only an evaluator-validated SAT witness.

Unsupported expressions and exhausted search return None, leaving the external solver as the authoritative fallback.