Nested quantifiers, such as ∀ int x, int y; 0 ≤ x < 5 ∧ 0 ≤ y < 3 ⇒ a[5y+x]>0, pose challenges for verification tools based on SMT solvers. An SMT solver cannot simply determine a[13]>0 using the quantifier, since it has trouble finding the correct values for x and y, in this case x=3 and y=2. The given quantifier is equivalent to ∀ int xy; 0 ≤ xy < 15 ⇒ a[xy]>0, which is a better fit for an SMT solver.

In our presentation, we introduce a general method to rewrite nested quantifiers in VerCors, a deductive verification tool based on separation logic. We validated this pattern in Lean, which helped resolve correctness issues in our initial version. We will discuss the auto-rewriting process in VerCors and discuss its necessity for parallel programs.