pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.03k stars 49 forks source link

Update Z3 version #248

Closed pschanely closed 4 months ago

pschanely commented 8 months ago

Our current version issues a deprecation warning. Noticed here.

IIRC, the only blocker here is that, under our current config, Z3 performs significantly worse in our benchmarks. I imagine this is fixable with additional Z3 configuration.

pschanely commented 7 months ago

Update: this likely is somewhat challenging to fix. It seems that something about the way CrossHair uses Z3 is causing aggressive memory leaks in more modern versions of Z3. (which may very well be the source of the slowness mentioned above)

I'll to a tiny investigation to see whether I can make a reproducible example. But I might end up just trying to pull the trigger on fully pluggable smtlib backends instead.

pschanely commented 4 months ago

Fixed in 0.0.55!