The search for optimal differential trails for ARX ciphers is known to be difficult and scale poorly as the word size (and the branching through the carries of modular additions) increases. To overcome this problem, one may approximate the modular addition with the XOR operation, a process called linearization. The immediate drawback of this approach is that many valid and good trails are discarded. In this work, we explore different partial linearization trade-offs to model the modular addition through the window heuristic, which restricts carry propagation to windows of \(w_s\) consecutive positions. This strategy enables the exploration of full linearization ( \(w_s = 0\) ), normal modelling ( \(w_s = n\) ), and all the different trade-offs between completeness and speed in between. We give the corresponding SAT and MILP model and their parallel versions, and apply them to ChaCha, SPECK, LEA, and HIGHT. Our method greatly outperforms all previous modeling of modular addition. In particular, we find the first differential path for 4 rounds of ChaCha with a probability greater than \(2^{-256}\) , and a corresponding 6 rounds boomerang distinguisher. This indicates that purely differential-based attacks have the potential to become competitive with differential-linear attacks, currently, the best-known attacks against ChaCha and other ARX ciphers. On SPECK, we find many improvements over the state-of-the-art in terms of speed of the differential trail search in the single-key setting and new upper bound probabilities in the related-key setting. Finally, we exhibit an improved key recovery attack on reduced LEA .