Function hard_arith_fallback_model 

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