[pschanely]

Looking at some of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair

Sadly, there aren't a lot of resources on how to use SMT solvers well.

[fovc]

Is there a place to find your notes?

[pschanely]

Sadly, mine largely aren't committed to words yet. I do have a small thing on implementing regular expressions: https://medium.com/@pschanely/modeling-python-regular-expres...

But there is so much to talk about: gotchas with quantifiers, mixing logics, multiplication, float conversions. I'll try to write up some more of my experiences if that's valuable for folks!