Z3 used to have an awesome, web-intro, that let you type expressions that were evaluated on servers at Microsoft research. Sadly, Python is riddled with so many security holes that it turned out to be impossible to sandbox the Z3 session. So, Microsoft took down those pages. Here's the HTML without all the cool executable stuff. Still very informative, but not as immediately gratifying.