Better way to generate terms satisfying some judgement in Redex

I'm aware of two efforts in Redex doing random generators with constraints:

1. redex-check's #:satisfying-form (as discussed, e.g., in this thread).
2. ESOP'15 paper “Making random judgements” (it has homepage).

I wonder if second effort was merged into the Redex distribution in some reusable form. Is there a preference I should give to any of the approaches (and why)?