This is an interactive SMT solver built on the Z3 solver. The original application was for the Embedded Device Generation project that I work on at Berkeley Lab11. It is meant to automatically validate and generate circuits based on a library of parts. I finished a minimum viable product in December 2020, and am working on fleshing it out and integrating it with the rest of the EDG system.