[G0lg0thvn]

z3py is going through python’s interpreter to talk to the c++ core of z3; this creates a performance bottleneck as the system size grows. The native input language of z3 is smt2, so coding in plain old python with type hints and then transpile to smt2 would, ideally, help with the bottleneck enabling solving of increasingly complex systems.

That’s how I understand it at least! Someone please correct me if I’m off base.