  Logically constrained rewrite systems (LCTRSs) are a versatile and efficient
rewriting formalism that can be used to model programs from various programming
paradigms, as well as simplification systems in compilers and SMT solvers. In
this paper, we investigate techniques to analyse the worst-case runtime
complexity of LCTRSs. For that, we exploit synergies between previously
developed decomposition techniques for standard term rewriting by Avanzini et
al. in conjunction with alternating time and size bound approximations for
integer programs by Brockschmidt et al. and adapt these techniques suitably to
LCTRSs. Furthermore, we provide novel modularization techniques to exploit loop
bounds from recurrence equations which yield sublinear bounds. We have
implemented the method in TCT to test the viability of our method.
