regehr et al use alive2 which uses z3