@Kuba forums.wolfram.com/mathgroup/archive/2006/Aug/msg00607.html

@halirutan Thanks ;)

@kirma Do you know of a way to link Mathematica with the Z3 running on the same machine (e.g. bindings)? After your post I tried Z3 via rise4fun.com. In the blink of an eye Z3 solved a problem Mathematica couldn't handle.

@halirutan It may be useful if you know how to handle resolution:

   CellPrint[
     Cell @@ MathLink`CallFrontEnd@
       FrontEnd`ConvertToBitmapPacket@
        Cell[BoxData@ToBoxes@Manipulate[x, {x, 0, 1}], "Output"]
     ]