Function eval_keccak_expr 

pub(crate) fn eval_keccak_expr(
    len: &Expr,
    bytes: &[Expr],
    model: &BTreeMap<String, U256>,
) -> Result<U256, SymbolicError>

Returns the concrete keccak value implied by a solver model.