ABSTRACT. We present Sloth, a solver for separation logic modulo theory constraints specified in the separation logic SL∗, a propositional separation logic that we recently introduced in our IJCAR'18 paper "A Separation Logic with Data: Small Models and Automation." SL∗ admits NP decision procedures despite its high expressiveness; features of the logic include support for list and tree fragments, universal data constraints about both lists and trees, and Boolean closure of spatial formulas. Sloth solves SL* constraints via an SMT encoding of SL* that is based on the logic's small-model property. We argue that, while clearly still a work in progress, Sloth already demonstrates that SL* lends itself to the automation of nontrivial examples. These results complement the theoretical work presented in the IJCAR'18 paper.