How to enumerate solutions using Z3

http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation

1) Find first solution, record it
2) Rerun SAT blocking the previous solution, find one more solution, record it
3) Rerun SAT blocking the first 2 solutions, and so forth.

Strange that SAT has to be repeated all over again each time. This is why enumeration takes time.

Need to:
1) Read DIMACS model, and run the above routine.
2) Not all the solutions will be useful. What I need is feature-rich solutions.