Function fallback_two_var_model 

pub(crate) fn fallback_two_var_model(
    constraints: &[SymBoolExpr],
) -> Option<HashMap<Symbol, U256>>