Hack, hack. Pass context to solver after defaulting.
Hack, hack. Pass context to solver after defaulting.

The structure of all this should be fixed.

GaloisInc/cryptol,GaloisInc/cryptol,GaloisInc/cryptol