can generate lists now with fixpoint-smt interface

there's an issue with the model refutation though. when we refute the
entire model, including concrete values and equivalence classes, z3
seems to strictly prefer shuffling the concrete values around. how to
reduce the bias?