Z3 was able to check equivalence of firewalls with a few hundred rules in a fraction of a second on a standard workstation. I was extremely impressed, especially since the brute-force IPv4 packet search space is 2^112! There's some wizardry going on beneath the hood.
On the network firewall rules (at multi-tenant Azure, I presume), what were Z3's runtimes look like?