AllSAT

In fact, it would be good to add a test for an expression that has a lot of models, and check the first few of them (a test that would take forever to finish if *all* models were actually computed). Maybe just a trivial expression with 100 variables or something.