Support for multiple satisfying assignments

[robdockins]

As I work on adding what4 as a new proof backend for Cryptol, one feature I notice that SBV supports that What4 currently does not is computing multiple satisfying assignments for a query.

Given the What4 programming model, it's not immediately clear what's the best way to provide this functionality.

[robdockins]

For now, this issue is solved in Cryptol by externally computing blocking predicates and issuing new queries. We might still consider some kind of support for multisat queries at some point, but it's not a critical issue at the moment.