Oh, I see. I had been confused about how to implement SMT integration because Ghidra's varnode concept did not seem to map very cleanly onto it. That is why, when I previously published some program analysis research using Ghidra, I said the following:

I still have one more thing to tackle before I feel comfortable recommending Ghidra wholeheartedly for automated binary program analysis. [...] For classical data flow analysis and abstract interpretation, I highly recommend it, though the jury is still out on SMT integration.

I did not get back to doing that research, as I have been largely focusing on C++ reverse engineering (and a training class thereupon) in the meantime. I was very curious to see how this project handled translating varnodes into SMT expressions. A bit of code review lead me here, which ultimately lead me here, and to my answer: they sidestep the concerns I had by working on the so-called "high" form of the PCode.

I'm glad somebody figured that out. Once I'm less busy, I'd like to continue with some Ghidra/SMT research I'd put aside pending the above information.