Check out angr [1], a symbolic execution engine, and claripy [2], its frontend to SMT solvers like z3. Depending on your background, I probably wouldn't describe angr as "for newbies," but claripy is a very clean SMT interface!

[1] https://angr.io

[2] https://api.angr.io/claripy.html