I've not. Firewall rules are of the form {predicate} -> {decision}, where {decision} is block/allow and {predicate} defines a set of packets: something like a source address range, source port range, destination address range, destination port range, and protocol. When a packet comes in, the firewall finds all matching predicates (there can be multiple) and makes a block/allow decision. Since checking for packet-predicate matches is done with simple and/or/not formulas, I can't think of a rule which could not be expressed in Z3. Also, this is hardly taxing Z3: it supports reasoning with real numbers and nonlinear constraints.