Hacker News Reader

Thanks again. I didn't know Z3 could handle formulae with real numbers. I will take a closer look at it. :)

On the network firewall rules (at multi-tenant Azure, I presume), what were Z3's runtimes look like?

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.

Reply on news.ycombinator.com