I released a version with an iterator for the default and exclusion semantics. It still needs some tuning since currently it doesn't find very many counterexamples, but the couterexamples are all non-isomorphic. The docs for these theories provide further details.