Out of curiosity, are there known pros and cons to each approach? I’ve been experimenting with Z3’s CHC engine and Coq for modeling programs. I don’t know enough about both yet to fully understand how they compare.