Verification-time slowdown after commit 2cc052c #6424
Description
We noticed a verification-time slowdown that appeared with 2cc052c and did not happen with its parent commit c931468. The slowdown persists in v4.11.0.
In c931468, the annotated program verifies in about 4 seconds, whereas in 2cc052c and v4.11.0 it doesn't finish verifying after 5 minutes. The solver version was fixed to Z3 v4.12.1 in all cases, and the OS was Ubuntu 20.04.
The minimized test is available here, and the slowdown is triggered by Dafny /functionSyntax:3 /compile:0 test.dfy.
@atomb @zafer-esen We're testing Dafny and looking for potential performance slowdowns across versions, and this commit came up during git bisect. We wanted to share it in case it's useful.