Performance regression with PyPI z3-solver Version 4.13.1.0 #7404
Description
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.