Z3: finding all satisfying models

One way to accomplish this is using one of the APIs, along with the model generation capability. You can then use the generated model from one satisfiability check to add constraints to prevent previous model values from being used in subsequent satisfiability checks, until there are no more satisfying assignments. Of course, you have to be using finite sorts (or have some constraints ensuring this), but you could use this with infinite sorts as well if you don't want to find all possible models (i.e., stop after you generate a bunch).

Here is an example using z3py (link to z3py script: http://rise4fun.com/Z3Py/a6MC ):

a = Int('a')
b = Int('b')

s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)

while s.check() == sat:
  print s.model()
  s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model

In general, using the disjunct of all the involved constants should work (e.g., a and b here). This enumerates all integer assignments for a and b (between 1 and 20) satisfying a >= 2b. For example, if we restrict a and b to lie between 1 and 5 instead, the output is:

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]