  We present a novel decision procedure for a fragment of separation logic (SL)
with arbitrary nesting of separating conjunctions with boolean conjunctions,
disjunctions, and guarded negations together with a support for the most common
variants of linked lists. Our method is based on a model-based translation to
SMT for which we introduce several optimisations$\unicode{x2013}$the most
important of them is based on bounding the size of predicate instantiations
within models of larger formulae, which leads to a much more efficient
translation of SL formulae to SMT. Through a series of experiments, we show
that, on the frequently used symbolic heap fragment, our decision procedure is
competitive with other existing approaches, and it can outperform them outside
the symbolic heap fragment. Moreover, our decision procedure can also handle
some formulae for which no decision procedure has been implemented so far.
