I've just built z3, a fast satisfiability modulo theory (SMT) solver by Microsoft, on openbsd 5.8.
And it was a breeze (git clone, make the make, make z3). It was such a breeze I thought it might make a good port for me to try making my first port with. Additionally it appears to be MIT licensed at present, which seems very compatible with BSD philosophy. So reading the documentation on porting , I wanted to communicate my intent and verify this is not already a port being worked on. So is anyone already working on a z3 port?