Neat! Author here. Pleasantly surprised to see this made it on here. You can find the corresponding video tutorial here https://www.youtube.com/watch?v=56IIrBZy

Neat! Author here. Pleasantly surprised to see this made it on here. You can find the corresponding video tutorial here https://www.youtube.com/watch?v=56IIrBZy9Rc&t=13s&ab_channel=BroadInstitute https://www.youtube.com/watch?v=56IIrBZy9Rc&t=13s&ab_channel... and github repo here https://github.com/philzook58/z3_tutorial https://github.com/philzook58/z3_tutorial and an assortment of blog posts from which I pulled some of the material of this tutorial here https://www.philipzucker.com/ https://www.philipzucker.com/ and a translation of some of this tutorial to Coq here https://www.philipzucker.com/translating-z3-to-coq/ https://www.philipzucker.com/translating-z3-to-coq/