Lots of changes to how sets are broken down, but still not quick enough.
Need to reduce # of calls to Z3. All basic tests passing again.