Thank you! I haven’t seen PropCheck before so I will make a note to add it to a list of related packages.
Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?
Other Languages’ SMT Packages (PySMT) do this! It’s a good thing to put on a roadmap. Z3.jl (there seem to be 2 but I’m familiar with this one) My main concern is it’s not well documented, so although I’ve used it I’m not confident in understanding it well enough to interface with it.
I use Base.process to talk with solvers but have had difficulty with pipes which I think is related to Julia issue #24717 and the state of two-way communication with long-lived external processes. So other ways to interface with solvers are a good idea, especially if they allow all the dependencies to be Pkg installed.