A hybrid SAT-based decision procedure for separation logic with uninterpreted functions