previous nightly 4.9.2+4ecc4bf1a679785bcd4fc444078d8064ffa085e3 created lots of zombie z3 processes on Mac M2

[kjx]

Failing code

N/A

Steps to reproduce the issue

work with dafny for a while

• Dafny version: 4.9.2.0
• Dafny VSCode extension version: 3.4.3

Expected behavior

when verification finishes, z3 processes go away

Actual behavior

302+z3 processes.
Popup window says out of application memory.

[keyboardDrummer]

Can you provide context? What's the workflow that led to this? Are the z3 processes child processes of another process? Which one?

[kjx]

workflow - running Dafny? the things just.. accumulate. seems they processes are children of "dotnet"

.ps -lcukjx | grep 6939
  501  6939  6928     4044   0  33  0 417260384  17648 -      S                   0 ??       114:25.69 dotnet
  501 53285  6939     4004   0  31  0 420333200    400 -      S                   0 ??         0:28.71 z3-4.12.1
  501 53300  6939     4004   0  31  0 416800448    400 -      S                   0 ??         0:28.55 z3-4.12.1
  501 53318  6939     4004   0  31  0 417475248    400 -      S                   0 ??         0:26.44 z3-4.12.1
  501 53322  6939     4004   0  31  0 417464896    400 -      S                   0 ??         0:26.47 z3-4.12.1
  501 53345  6939     4004   0  31  0 417468432    400 -      S                   0 ??         0:26.98 z3-4.12.1
  501 53462  6939     4004   0  31  0 419833120    400 -      S                   0 ??         0:28.86 z3-4.12.1
  501 53720  6939     4004   0  31  0 419850752    400 -      S                   0 ??         0:27.80 z3-4.12.1
  501 53772  6939     4004   0  31  0 419439040    400 -      S                   0 ??         0:28.52 z3-4.12.1
  501 53812  6939     4004   0  31  0 418382256    400 -      S                   0 ??         0:28.25 z3-4.12.1
  501 53975  6939     4004   0  31  0 420103632    400 -      S                   0 ??         0:27.94 z3-4.12.1
  501 54078  6939     4004   0  31  0 415539168    416 -      S                   0 ??         0:29.21 z3-4.12.1
  501 54489  6939     4004   0  31  0 410824992    432 -      S                   0 ??         0:00.34 z3-4.12.1
  501 54490  6939     4004   0  31  0 410693920    432 -      S                   0 ??         0:00.21 z3-4.12.1
  501 54492  6939     4004   0  31  0 410693920    432 -      S                   0 ??         0:00.30 z3-4.12.1
  501 54493  6939     4004   0  31  0 410824992    432 -      S                   0 ??         0:00.24 z3-4.12.1
  501 54496  6939     4004   0  31  0 410693920    432 -      S                   0 ??         0:00.11 z3-4.12.1

[keyboardDrummer]

running Dafny?

Using the CLI or the IDE? Is your verification timing out? Is there a specific step you can do to get an extra process?

The reason I ask is that generally, the Dafny IDE and CLI do clean up their Z3 processes. Also for verification that times out, the IDE will still terminate the Z3 process. There must be something specific that is triggering this problem in your case, and right now I don't have many leads to go on.