Performance regression with PyPI z3-solver Version 4.13.1.0

[iamnotthatbob]

Things got a lot slower (~100x time required) with the latest version published a few hours ago. Here's the code I used to test:

from z3 import *

s = Solver()
x, y = Reals('x y')
s.add(y == x * x + 3 * x + 1, y == 0)
print(s.check())
pp(s.model())
pp(s.statistics())

Output for latest version (4.13.1.0)

sat
[x = -2.6180339887?, y = 0]
(:max-memory                   209.04
 :memory                       188.33
 :nlsat-irrational-assignments 1
 :nlsat-propagations           2
 :nlsat-restarts               1
 :nlsat-stages                 2
 :num-allocs                   1576074882
 :rlimit-count                 328
 :solve-eqs-elim-vars          1
 :solve-eqs-steps              1
 :time                         1.75)

Output for the last version (4.13.0.0)

sat
[x = -2.6180339887?, y = 0]
(:max-memory                   24.79
 :memory                       24.12
 :nlsat-irrational-assignments 1
 :nlsat-propagations           2
 :nlsat-stages                 2
 :num-allocs                   10529528
 :rlimit-count                 20791
 :solve-eqs-elim-vars          1
 :solve-eqs-steps              1
 :time                         0.01)

I ran the same thing multiple times on both versions, and the outputs are all in their respective ballpark. It seems like the latest version is doing a lot more allocations for some reason.

[iamnotthatbob]

Can confirm it returned to normal in version 4.13.2.0. Thanks for fixing it so quickly!