Just a ticket to keep track of the DA related issues, which will be addressed next: - [ ] #3213 Using Z3 for better DA - [ ] #3225 Incorrectly parallelised loop using structures (`a` and `a%b`, which the DA considers to be different) - [ ] #3225 Using `a(i/2)` is parallelised - [ ] #3224 Outer loop cannot be parallelised because two consecutive inner loops are detected to be dependent.