I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even if it is orders of magnitude less complex than z3.

I don't think the concept of SMT is has to be tied to classical logic in some abstract sense, but the SMTlib standard is classical. And in the sense that an SMT solver is SAT solver (kind of as classical as you can get) bolted to theories. But seems reasonable to build some kind of framework bolting domain specific intuitionistic solvers to a intuitionistic fabric.

See Itauto https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.I... https://gitlab.inria.fr/fbesson/itauto which would be another interesting backend. Reusing tactics from other systems is maybe just a step too far for knuckledragger in terms of packaging and interfacing problems