That was interesting - never seen Z3 applied for verification of networking and cryptographic algorithms.

My team similarly used Z3 to reverse-generate data from SQL queries so that erroneous mutations of the queries get detected early on: http://www.cse.iitb.ac.in/infolab/xdata/